git.iko.soy/Idris-dev
on master help sign in
Normalise local variable types in metavariables
commitbf52728c57bf0f51e3042d2191808cd6e7f54a84 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 25 Jul 2015, 18:12 (11 years ago) parent6b062be
1 file changed+2−2
compare with master
unifiedsplit
src/Idris/Elab/Term.hs+2−2
src/Idris/Elab/Term.hs+2−2
@@ -1818,12 +1818,12 @@ collectDeferred top casenames ctxt (Bind n (GHole i t) app) =
18181818 tidy ctxt env t | (f, args) <- unApply t,
18191819 P _ specn _ <- getFn f,
18201820 n `notElem` casenames
1821− = fst $ specialise ctxt env [(specn, 99999)] t
1821+ = normalise ctxt env t
18221822 tidy ctxt env t@(Bind n (Let _ _) sct)
18231823 | (f, args) <- unApply sct,
18241824 P _ specn _ <- getFn f,
18251825 n `notElem` casenames
1826− = fst $ specialise ctxt env [(specn, 99999)] t
1826+ = normalise ctxt env t
18271827 tidy ctxt env t = t
18281828
18291829 getFn (Bind n (Lam _) t) = getFn t