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

8 files changed, 18 insertions, 19 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 4617f4dee4..3953623885 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -13,6 +13,13 @@ efficiency, when an evar is known to be undefined, it is preferable to
 use specific functions about undefined evars since these ones are
 generally fewer than the defined ones.
 
+** Type changes 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 via
+Tacinterp.eval_tactic.
+
 =========================================
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 9cafb79f73..e1ae919663 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -42,12 +42,6 @@ let rec make_let e = function
       let loc = join_loc loc (MLast.loc_of_expr e) in
       let e = make_let e l in
       let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in
-      let v =
-        (* Special case for tactics which must be stored in algebraic
-           form to avoid marshalling closures and to be reprinted *)
-        if is_tactic_genarg t then
-          <:expr< ($v$, Tacinterp.eval_tactic $v$) >>
-        else v in
       <:expr< let $lid:p$ = $v$ in $e$ >>
   | _::l -> make_let e l
 
@@ -85,9 +79,7 @@ let rec make_eval_tactic e = function
       let p = Names.string_of_id p in
       let loc = join_loc loc (MLast.loc_of_expr e) in
       let e = make_eval_tactic e l in
-        (* Special case for tactics which must be stored in algebraic
-           form to avoid marshalling closures and to be reprinted *)
-      <:expr< let $lid:p$ = ($lid:p$,Tacinterp.eval_tactic $lid:p$) in $e$ >>
+      <:expr< let $lid:p$ = $lid:p$ in $e$ >>
   | _::l -> make_eval_tactic e l
 
 let rec make_fun e = function
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 200c52efc1..9873d2d5a3 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -432,7 +432,7 @@ TACTIC EXTEND fauto
     [ "fauto" tactic(tac)] ->
       [
 	let heuristic = chose_heuristic None in
-	finduction None heuristic (snd tac)
+	finduction None heuristic (Tacinterp.eval_tactic tac)
       ]
   |
     [ "fauto" ] ->
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index d6100a15b0..1f4ea97fd1 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -13,7 +13,7 @@ open Tacexpr
 open Quote
 
 let make_cont k x =
-  let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> fst k)) in
+  let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> k)) in
   let x = TacDynamic(dummy_loc, Pretyping.constr_in x) in
   let tac = <:tactic<let cont := $k in cont $x>> in
   Tacinterp.interp tac
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 741d22a8a7..64cfa0d01c 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -831,7 +831,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
 
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
-    [ let (t,lr) = list_sep_last lrt in ring_lookup (fst f) lH lr t]
+    [ let (t,lr) = list_sep_last lrt in ring_lookup f lH lr t]
 END
 
 
@@ -1159,5 +1159,5 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl =
 
 TACTIC EXTEND field_lookup
 | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
-      [ let (t,l) = list_sep_last lt in field_lookup (fst f) lH l t ]
+      [ let (t,l) = list_sep_last lt in field_lookup f lH l t ]
 END
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