Merge pull request #2432 from bkoropoff/fix-case-tac-reflection
Fix copy-paste bug when reifying reflected tactics
commitc86483754dfcbf244fca1fde5d5189693c0f993d
authorDavid Christiansen <david@davidchristiansen.dk>
dateSun 12 Jul 2015, 21:13 (11 years ago)
parent3d222a1cf9f36b
src/Idris/Reflection.hs+1−1
@@ -88,7 +88,7 @@ reifyApp ist t [Constant (Str n), x]
8888 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
8989reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
9090reifyApp 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')
9292reifyApp ist t [t']
9393 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
9494reifyApp ist t [t']