git.iko.soy/Idris-dev
on master help sign in
Minor rewording of error message
commit7dca9b416ee663391145af241381a795a2997f37 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 31 May 2015, 19:57 (11 years ago) parent6c48da8
2 files changed+4−4
compare with master
unifiedsplit
src/Idris/Delaborate.hs+3−3 src/Idris/Interactive.hs+1−1
src/Idris/Delaborate.hs+3−3
@@ -346,19 +346,19 @@ pprintErr' i (AlreadyDefined n) = annName n<+>
346346pprintErr' i (ProofSearchFail e) = pprintErr' i e
347347pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delab i tm))
348348pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
349−pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
349+pprintErr' i (Elaborating s n e) = text "When checking" <+> text s <>
350350 annName' n (showqual i n) <> colon <$>
351351 pprintErr' i e
352352pprintErr' i (ElaboratingArg f x _ e)
353353 | isInternal f = pprintErr' i e
354354 | isUN x =
355− text "When elaborating argument" <+>
355+ text "When checking argument" <+>
356356 annotate (AnnBoundName x False) (text (showbasic x)) <+> -- TODO check plicity
357357 -- Issue #1591 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1591
358358 text "to" <+> whatIsName <> annName f <> colon <>
359359 indented (pprintErr' i e)
360360 | otherwise =
361− text "When elaborating an application of" <+> whatIsName <>
361+ text "When checking an application of" <+> whatIsName <>
362362 annName f <> colon <> indented (pprintErr' i e)
363363 where whatIsName = let ctxt = tt_ctxt i
364364 in if isTConName f ctxt
src/Idris/Interactive.hs+1−1
@@ -162,7 +162,7 @@ makeWith fn updatefile l n
162162doProofSearch :: FilePath -> Bool -> Bool ->
163163 Int -> Name -> [Name] -> Maybe Int -> Idris ()
164164doProofSearch fn updatefile rec l n hints Nothing
165− = doProofSearch fn updatefile rec l n hints (Just 10)
165+ = doProofSearch fn updatefile rec l n hints (Just 20)
166166doProofSearch fn updatefile rec l n hints (Just depth)
167167 = do src <- runIO $ readSource fn
168168 let (before, tyline : later) = splitAt (l-1) (lines src)