Fix copy-paste bug when reifying reflected tactics
Map `Case` to `CaseTac` (not `Induction`)
commitcf9f36be662a68ac871c9d6f1b4a2c5442f21862
authorBrian Koropoff <bkoropoff@gmail.com>
dateSat 11 Jul 2015, 23:49 (11 years ago)
parent7831e10
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']