diff options
Diffstat (limited to 'tactics/newtauto.ml4')
| -rw-r--r-- | tactics/newtauto.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/newtauto.ml4 b/tactics/newtauto.ml4 index 11958a0ea..0c8f9bb4a 100644 --- a/tactics/newtauto.ml4 +++ b/tactics/newtauto.ml4 @@ -226,12 +226,12 @@ let lfo_wrap n gl= TACTIC EXTEND NewIntuition [ "NewIntuition" ] -> [ newtauto true default_stac ] - |[ "NewIntuition" tactic(t)] -> [ newtauto true (interp t) ] + |[ "NewIntuition" tactic(t)] -> [ newtauto true (snd t) ] END TACTIC EXTEND Intuition1 [ "Intuition1" ] -> [ newtauto false default_stac ] - |[ "Intuition1" tactic(t)] -> [ newtauto false (interp t) ] + |[ "Intuition1" tactic(t)] -> [ newtauto false (snd t) ] END TACTIC EXTEND NewTauto |