git.iko.soy/Idris-dev
on master help sign in
Resolve names/expand implicits inside refl
ecb42f0Edwin Brady
src/Idris/AbsSyntax.hs+1
compare with master
unifiedsplit
@@ -1029,6 +1029,7 @@ addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm
1029 ai env (PHidden tm) = PHidden (ai env tm)
1029 ai env (PHidden tm) = PHidden (ai env tm)
1030 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1030 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
1031 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1031 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)
1032+ ai env (PRefl fc tm) = PRefl fc (ai env tm)
1032 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1033 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)
1033 ai env tm = tm
1034 ai env tm = tm
1034
1035
src/Idris/Delaborate.hs+1−1
@@ -102,7 +102,7 @@ pshow i (CantUnify _ x y e sc s)
102 = let imps = opt_showimp (idris_options i) in
102 = let imps = opt_showimp (idris_options i) in
103 "Can't unify " ++ showImp imps (delab i x)
103 "Can't unify " ++ showImp imps (delab i x)
104 ++ " with " ++ showImp imps (delab i y) ++
104 ++ " with " ++ showImp imps (delab i y) ++
105−-- " (" ++ show x ++ " and " ++ show y ++ ") " ++
105+-- " (" ++ showEnvDbg [] x ++ " and " ++ showEnvDbg [] y ++ ") " ++
106 case e of
106 case e of
107 Msg "" -> ""
107 Msg "" -> ""
108 _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++
108 _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++