git.iko.soy/Idris-dev
on master help sign in
Fixes a problem with custom tactics using Intro & Induction

Intro would previously fail with "Unknown Tactic".

commit1f6e885ac635c8151f9de1116d8b475036a26ed0 authorJonathan Sterling <jonsterling@me.com> dateThu 24 Apr 2014, 13:14 (13 years ago) parent9abed6a
1 file changed+2−2
compare with master
unifiedsplit
src/Idris/ElabTerm.hs+2−2
src/Idris/ElabTerm.hs+2−2
@@ -1184,8 +1184,8 @@ reifyApp _ t [x]
11841184reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
11851185reifyApp ist t [Constant (Str n), x]
11861186 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
1187−reifyApp _ t [Constant (Str n)]
1188− | t == reflm "Intro" = return $ Intro [sUN n]
1187+reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
1188+reifyApp _ t [n] | t == reflm "Induction" = liftM Induction (reifyTTName n)
11891189reifyApp ist t [t']
11901190 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
11911191reifyApp ist t [t']