diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 8 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 36fa43ff25..c86ab581bb 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -100,7 +100,7 @@ let progress_evars t gl = in tclTHEN t check gl TACTIC EXTEND progress_evars - [ "progress_evars" tactic(t) ] -> [ progress_evars (snd t) ] + [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.eval_tactic t) ] END let unify_e_resolve flags (c,clenv) gls = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 8955b6c7e8..0490f1bc89 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -193,7 +193,7 @@ TACTIC EXTEND autorewrite | [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] -> [ let cl = glob_in_arg_hyp_to_clause cl in - auto_multi_rewrite_with (snd t) l cl + auto_multi_rewrite_with (Tacinterp.eval_tactic t) l cl ] END @@ -203,7 +203,7 @@ TACTIC EXTEND autorewrite_star [ auto_multi_rewrite ~conds:AllMatches l (glob_in_arg_hyp_to_clause cl) ] | [ "autorewrite" "*" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] -> [ let cl = glob_in_arg_hyp_to_clause cl in - auto_multi_rewrite_with ~conds:AllMatches (snd t) l cl ] + auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.eval_tactic t) l cl ] END (**********************************************************************) @@ -465,12 +465,12 @@ let add_transitivity_lemma left lem = (* Vernacular syntax *) TACTIC EXTEND stepl -| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (snd tac) ] +| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.eval_tactic tac) ] | ["stepl" constr(c) ] -> [ step true c tclIDTAC ] END TACTIC EXTEND stepr -| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (snd tac) ] +| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.eval_tactic tac) ] | ["stepr" constr(c) ] -> [ step false c tclIDTAC ] END diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index b493d989b3..a9d4bd8899 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -297,5 +297,5 @@ END TACTIC EXTEND intuition | [ "intuition" ] -> [ intuition_gen default_intuition_tac ] -| [ "intuition" tactic(t) ] -> [ intuition_gen (fst t) ] +| [ "intuition" tactic(t) ] -> [ intuition_gen t ] END |