diff options
| author | glondu | 2010-09-30 18:45:31 +0000 |
|---|---|---|
| committer | glondu | 2010-09-30 18:45:31 +0000 |
| commit | 9a7da63b880cbeb3e58af5b2e0b39afcd650c253 (patch) | |
| tree | 11cd51860193fd59d7550b4804246bddea1e9d79 /tactics | |
| parent | 77e3ca28bbac9d973fbf0c5cd36de58159356710 (diff) | |
Simplify tactic(_)-bound arguments in TACTIC EXTEND rules
Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type
glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first
component is kept, the second one can be obtained with
Tacinterp.eval_tactic.
Rationale: these declare parsing rules, and eval_tactic is a semantic
action, and therefore should be done in the rule body
instead. Moreover, having the glob_tactic_expr and its evaluation
captured by these rules was quite confusing IMHO.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13480 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |