Applying Tom Prince's patch to support parametric "constructor n" in

tactic notations and ltac definitions (see bug report #2496).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14606 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 12 insertions, 16 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9f4b10575e..f1b3ffed42 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -218,12 +218,6 @@ GEXTEND Gram
       (* This is used in quotations *)
       | id = METAIDENT -> MetaId (loc,id) ] ]
   ;
-  (* A number or a quotation meta-variable *)
-  num_or_meta:
-    [ [ n = integer -> AI n
-      |	id = METAIDENT -> MetaId (loc,id)
-      ] ]
-  ;
   open_constr:
     [ [ c = constr -> ((),c) ] ]
   ;
@@ -638,9 +632,9 @@ GEXTEND Gram
       | "exists"; bll = LIST1 opt_bindings SEP "," -> TacSplit (false,true,bll)
       | IDENT "eexists"; bll = LIST1 opt_bindings SEP "," ->
 	  TacSplit (true,true,bll)
-      | IDENT "constructor"; n = num_or_meta; l = with_bindings ->
+      | IDENT "constructor"; n = nat_or_var; l = with_bindings ->
 	  TacConstructor (false,n,l)
-      | IDENT "econstructor"; n = num_or_meta; l = with_bindings ->
+      | IDENT "econstructor"; n = nat_or_var; l = with_bindings ->
 	  TacConstructor (true,n,l)
       | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor (false,t)
       | IDENT "econstructor"; t = OPT tactic -> TacAnyConstructor (true,t)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index b781e4e6e2..fd4c1bcea0 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -788,7 +788,7 @@ and pr_atom1 = function
   | TacAnyConstructor (ev,None) as t -> pr_atom0 t
   | TacConstructor (ev,n,l) ->
       hov 1 (str (with_evars ev "constructor") ++
-             pr_or_metaid pr_intarg n ++ pr_bindings l)
+             pr_or_var pr_intarg n ++ pr_bindings l)
 
   (* Conversion *)
   | TacReduce (r,h) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a155015b5f..e184eafe37 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -381,7 +381,7 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacAnyConstructor (ev,t) ->
       <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_bool ev$ $mlexpr_of_option mlexpr_of_tactic t$>>
   | Tacexpr.TacConstructor (ev,n,l) ->
-      let n = mlexpr_of_or_metaid mlexpr_of_int n in
+      let n = mlexpr_of_or_var mlexpr_of_int n in
       <:expr< Tacexpr.TacConstructor $mlexpr_of_bool ev$ $n$ $mlexpr_of_binding_kind l$>>
 
   (* Conversion *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 1928f5853d..9e2acfdd05 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -191,7 +191,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
   | TacRight of evars_flag * 'constr bindings
   | TacSplit of evars_flag * split_flag * 'constr bindings list
   | TacAnyConstructor of evars_flag * 'tac option
-  | TacConstructor of evars_flag * int or_metaid * 'constr bindings
+  | TacConstructor of evars_flag * int or_var * 'constr bindings
 
   (* Conversion *)
   | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id gclause
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index c5a2f87b6e..fafc681ae2 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -111,9 +111,9 @@ let h_any_constructor t =
   abstract_tactic (TacAnyConstructor t) (any_constructor t)
 *)
 let h_constructor ev n l =
-  abstract_tactic (TacConstructor(ev,AI n,l))(constructor_tac ev None n l)
+  abstract_tactic (TacConstructor(ev,ArgArg n,l))(constructor_tac ev None n l)
 let h_one_constructor n =
-  abstract_tactic (TacConstructor(false,AI n,NoBindings)) (one_constructor n NoBindings)
+  abstract_tactic (TacConstructor(false,ArgArg n,NoBindings)) (one_constructor n NoBindings)
 let h_simplest_left   = h_left false NoBindings
 let h_simplest_right  = h_right false NoBindings
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d0fcad21a9..a88c5f79b7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -762,7 +762,7 @@ let rec intern_atomic lf ist x =
   | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl)
   | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (intern_bindings ist) bll)
   | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_tactic ist) t)
-  | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,intern_bindings ist bl)
+  | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl)
 
   (* Conversion *)
   | TacReduce (r,cl) ->
@@ -2323,7 +2323,7 @@ and interp_atomic ist gl tac =
         (Tactics.any_constructor ev (Option.map (interp_tactic ist) t))
   | TacConstructor (ev,n,bl) ->
       let sigma, bl = interp_bindings ist env sigma bl in
-      tclWITHHOLES ev (h_constructor ev (skip_metaid n)) sigma bl
+      tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl
 
   (* Conversion *)
   | TacReduce (r,cl) ->
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index a9d4bd8899..46f8c9bb4b 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -152,10 +152,12 @@ let flatten_contravariant_disj ist =
 	let hyp = valueIn (VConstr ([],hyp)) in
 	iter_tac (list_map_i (fun i arg ->
 	  let typ = valueIn (VConstr ([],mkArrow arg c)) in
+	  let i = Tacexpr.Integer i in
 	  <:tactic<
             let typ := $typ in
             let hyp := $hyp in
-	    assert typ by (intro; apply hyp; constructor $i; assumption)
+	    let i := $i in
+	    assert typ by (intro; apply hyp; constructor i; assumption)
 	  >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
       else
 	<:tactic<fail>>