git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2226 from david-christiansen/wip/tactical
e2915e7David Christiansen
src/Idris/CaseSplit.hs+1−1
compare with master
unifiedsplit
@@ -69,7 +69,7 @@ split n t'
69 let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
69 let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
70 let ctxt = tt_ctxt ist
70 let ctxt = tt_ctxt ist
71 case lookup n pats of
71 case lookup n pats of
72− Nothing -> fail $ show n ++ " is not a pattern variable"
72+ Nothing -> ifail $ show n ++ " is not a pattern variable"
73 Just ty ->
73 Just ty ->
74 do let splits = findPats ist ty
74 do let splits = findPats ist ty
75 iLOG ("New patterns " ++ showSep ", "
75 iLOG ("New patterns " ++ showSep ", "
src/Idris/Delaborate.hs+4−3
@@ -382,10 +382,11 @@ pprintErr' i (ReflectionFailed msg err) =
382 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
382 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
383pprintErr' i (ElabScriptDebug msg tm holes) =
383pprintErr' i (ElabScriptDebug msg tm holes) =
384 text "Elaboration halted." <>
384 text "Elaboration halted." <>
385− maybe empty (indented . text) msg <> line <>
385+ maybe empty (indented . text) msg <>
386− text "Term: " <> indented (pprintTT [] tm) <> line <>
386+ line <> line <>
387 text "Holes:" <>
387 text "Holes:" <>
388− indented (vsep (map ppHole holes))
388+ indented (vsep (map ppHole holes)) <> line <> line <>
389+ text "Term: " <> indented (pprintTT [] tm)
389
390
390 where ppHole :: (Name, Type, Env) -> Doc OutputAnnotation
391 where ppHole :: (Name, Type, Env) -> Doc OutputAnnotation
391 ppHole (hn, goal, env) =
392 ppHole (hn, goal, env) =