git.iko.soy/Idris-dev
on master help sign in
Make "Can't solve goal" more meaningful
commit50f4c824bfd200a1fc79023043e56910c3a45c80 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 8 Feb 2016, 08:49 (11 years ago) parente55fe2f
1 file changed+1−1
compare with master
unifiedsplit
src/Idris/Delaborate.hs+1−1
src/Idris/Delaborate.hs+1−1
@@ -317,7 +317,7 @@ pprintErr' i (CantConvert x_in y_in env) =
317317 flagUnique (Bind n b sc) = Bind n (fmap flagUnique b) (flagUnique sc)
318318 flagUnique t = t
319319pprintErr' i (CantSolveGoal x env) =
320− text "Can't solve goal " <>
320+ text "Can't find a value of type " <>
321321 indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delabSugared i x))) <>
322322 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
323323pprintErr' i (UnifyScope n out tm env) =