@@ -88,7 +88,7 @@ reifyApp ist t [Constant (Str n), x]
88 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
88 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
89reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
89reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
90reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
90reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
91−reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')
91+reifyApp ist t [t'] | t == reflm "Case" = liftM (CaseTac . delab ist) (reifyTT t')
92reifyApp ist t [t']
92reifyApp ist t [t']
93 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
93 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
94reifyApp ist t [t']
94reifyApp ist t [t']