git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1130 from jonsterling/fix/reify-intro-induction

Fixes a problem with custom tactics using Intro & Induction

commitfd1219b20649d947f9b854b560b4c946720e8c4a authorEdwin Brady <edwin.brady@gmail.com> dateWed 30 Apr 2014, 14:47 (12 years ago) parent4ed706a1f6e885
1 file changed+2−2
compare with master
unifiedsplit
src/Idris/ElabTerm.hs+2−2
src/Idris/ElabTerm.hs+2−2
@@ -1187,8 +1187,8 @@ reifyApp _ t [x]
11871187reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
11881188reifyApp ist t [Constant (Str n), x]
11891189 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
1190−reifyApp _ t [Constant (Str n)]
1191− | t == reflm "Intro" = return $ Intro [sUN n]
1190+reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
1191+reifyApp _ t [n] | t == reflm "Induction" = liftM Induction (reifyTTName n)
11921192reifyApp ist t [t']
11931193 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
11941194reifyApp ist t [t']