ecb42f0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Resolve names/expand implicits inside refl

Fixes #447

commitecb42f07afc25fc0a2cb28269fa87af35d8804e4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 8 Aug 2013, 17:07 (13 years ago) parent680dcf7

2 files changed+2−1

unifiedsplit

src/Idris/AbsSyntax.hs+1

@@ -1029,6 +1029,7 @@ addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm

10291029 ai env (PHidden tm) = PHidden (ai env tm)

10301030 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)

10311031 ai env (PTactics ts) = PTactics (map (fmap (ai env)) ts)

1032+ ai env (PRefl fc tm) = PRefl fc (ai env tm)

10321033 ai env (PUnifyLog tm) = PUnifyLog (ai env tm)

10331034 ai env tm = tm

10341035

src/Idris/Delaborate.hs+1−1

@@ -102,7 +102,7 @@ pshow i (CantUnify _ x y e sc s)

102102 = let imps = opt_showimp (idris_options i) in

103103 "Can't unify " ++ showImp imps (delab i x)

104104 ++ " with " ++ showImp imps (delab i y) ++

105−-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

105+-- " (" ++ showEnvDbg [] x ++ " and " ++ showEnvDbg [] y ++ ") " ++

106106 case e of

107107 Msg "" -> ""

108108 _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++