git.iko.soy/Idris-dev
on master help sign in
Give pi bindings unique names
1309a42Edwin Brady
src/Idris/ElabDecls.hs+2−1
compare with master
unifiedsplit
@@ -556,7 +556,8 @@ elab ist info pattern tm
556 elab' (PPi _ n ty sc)
556 elab' (PPi _ n ty sc)
557 = do attack; tyn <- unique_hole (MN 0 "ty")
557 = do attack; tyn <- unique_hole (MN 0 "ty")
558 claim tyn (RSet 0)
558 claim tyn (RSet 0)
559+ n' <- unique_hole n
559− forall n (Var tyn)
560+ forall n' (Var tyn)
560 focus tyn
561 focus tyn
561 elabE ty
562 elabE ty
562 elabE sc
563 elabE sc