git.iko.soy/Idris-dev
on master help sign in
refsIn should take all the Ps
8628481Edwin Brady
src/Idris/Core/TT.hs+1−1
compare with master
unifiedsplit
@@ -1416,7 +1416,7 @@ orderPats tm = op [] tm
1416
1416
1417refsIn :: TT Name -> [Name]
1417refsIn :: TT Name -> [Name]
1418refsIn (P _ n _) = [n]
1418refsIn (P _ n _) = [n]
1419−refsIn (Bind n b t) = nub $ nb b ++ (refsIn t \\ [n])
1419+refsIn (Bind n b t) = nub $ nb b ++ refsIn t
1420 where nb (Let t v) = nub (refsIn t) ++ nub (refsIn v)
1420 where nb (Let t v) = nub (refsIn t) ++ nub (refsIn v)
1421 nb (Guess t v) = nub (refsIn t) ++ nub (refsIn v)
1421 nb (Guess t v) = nub (refsIn t) ++ nub (refsIn v)
1422 nb t = refsIn (binderTy t)
1422 nb t = refsIn (binderTy t)