Changement du type d'argument 'TacticArgType X' en un type

'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de
pouvoir typer correctement les wit_tactic (auparavant le typage des
wit_tactic était trop libéral et permettait de casser la
subject-reduction).

Amélioration au passage de l'affichage de la tactique "replace by" 
(module Extratactics).



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

7 files changed, 103 insertions, 14 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index d1f82c1d99..a4239713b6 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -30,7 +30,6 @@ let rec make_rawwit loc = function
   | ConstrArgType -> <:expr< Genarg.rawwit_constr >>
   | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >>
   | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >>
-  | TacticArgType n -> <:expr< Genarg.rawwit_tactic $mlexpr_of_int n$ >>
   | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
   | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >>
@@ -56,7 +55,6 @@ let rec make_globwit loc = function
   | SortArgType -> <:expr< Genarg.globwit_sort >>
   | ConstrArgType -> <:expr< Genarg.globwit_constr >>
   | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >>
-  | TacticArgType n -> <:expr< Genarg.globwit_tactic  $mlexpr_of_int n$ >>
   | RedExprArgType -> <:expr< Genarg.globwit_red_expr >>
   | OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >>
@@ -82,7 +80,6 @@ let rec make_wit loc = function
   | SortArgType -> <:expr< Genarg.wit_sort >>
   | ConstrArgType -> <:expr< Genarg.wit_constr >>
   | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
-  | TacticArgType n -> <:expr< Genarg.wit_tactic $mlexpr_of_int n$ >>
   | RedExprArgType -> <:expr< Genarg.wit_red_expr >>
   | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
@@ -193,6 +190,9 @@ let rec interp_entry_name loc s =
     OptArgType t, <:expr< Gramext.Sopt $g$ >>
   else 
     let t, se =
+      if tactic_genarg_level s <> None then
+        Some (ExtraArgType s), <:expr< Tactic. tactic >>
+      else
       match Pcoq.entry_type (Pcoq.get_univ "prim") s with
 	| Some _ as x -> x, <:expr< Prim. $lid:s$ >>
 	| None -> 
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index f7127ea616..bc351cbaa8 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -210,7 +210,7 @@ let rec interp_entry_name up_level u s =
   else
     try 
       let i = find_index "tactic" s in
-      TacticArgType i, 
+      ExtraArgType s, 
       if i=up_level then Gramext.Sself else
       if i=up_level-1 then Gramext.Snext else
       Gramext.Snterml(Pcoq.Gram.Entry.obj Tactic.tactic_expr,string_of_int i)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index cb45a9f453..5c6216687a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -286,6 +286,55 @@ let force_entry_type (u, utab) s etyp =
   with Not_found -> 
     new_entry etyp (u, utab) s
 
+(* Tactics as arguments *)
+
+let tactic_main_level = 5
+
+let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg "tactic0"
+let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg "tactic1"
+let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg "tactic2"
+let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg "tactic3"
+let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg "tactic4"
+let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg "tactic5"
+
+let wit_tactic = function
+  | 0 -> wit_tactic0
+  | 1 -> wit_tactic1
+  | 2 -> wit_tactic2
+  | 3 -> wit_tactic3
+  | 4 -> wit_tactic4
+  | 5 -> wit_tactic5
+  | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+
+let globwit_tactic = function
+  | 0 -> globwit_tactic0
+  | 1 -> globwit_tactic1
+  | 2 -> globwit_tactic2
+  | 3 -> globwit_tactic3
+  | 4 -> globwit_tactic4
+  | 5 -> globwit_tactic5
+  | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+
+let rawwit_tactic = function
+  | 0 -> rawwit_tactic0
+  | 1 -> rawwit_tactic1
+  | 2 -> rawwit_tactic2
+  | 3 -> rawwit_tactic3
+  | 4 -> rawwit_tactic4
+  | 5 -> rawwit_tactic5
+  | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+
+let tactic_genarg_level s =
+  if String.length s = 7 && String.sub s 0 6 = "tactic" then
+    let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48)
+    else None
+  else None
+
+let is_tactic_genarg = function
+| ExtraArgType s -> tactic_genarg_level s <> None
+| _ -> false
+
+
 (* [make_gen_entry] builds entries extensible by giving its name (a string) *)
 (* For entries extensible only via the ML name, Gram.Entry.create is enough *)
 
@@ -382,7 +431,6 @@ module Tactic =
     let tactic_arg = Gram.Entry.create "tactic:tactic_arg"
     let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
 
-    let tactic_main_level = 5
     let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic"
 
     (* Main entry for quotations *)
@@ -391,6 +439,7 @@ module Tactic =
   end
 
 
+
 module Vernac_ =
   struct
     let gec_vernac s = Gram.Entry.create ("vernac:" ^ s)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 690810d8ab..404f3ab90d 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -81,6 +81,42 @@ val create_generic_entry : string -> ('a, rlevel,raw_tactic_expr) abstract_argum
 val get_generic_entry : string -> grammar_object Gram.Entry.e
 val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type
 
+(* Tactics as arguments *)
+
+val tactic_main_level : int
+
+val rawwit_tactic : int -> (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic : int -> (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic : int -> (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic0 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic0 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic0 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic1 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic1 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic1 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic2 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic2 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic2 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic3 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic3 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic3 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic4 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic4 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic4 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic5 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic5 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic5 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val is_tactic_genarg : argument_type -> bool
+
+val tactic_genarg_level : string -> int option
+
 (* The main entry: reads an optional vernac command *)
 
 val main_entry : (loc * vernac_expr) option Gram.Entry.e
@@ -148,7 +184,6 @@ module Tactic :
     val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e
     val tactic_arg : raw_tactic_arg Gram.Entry.e
     val tactic_expr : raw_tactic_expr Gram.Entry.e
-    val tactic_main_level : int
     val tactic : raw_tactic_expr Gram.Entry.e
     val tactic_eoi : raw_tactic_expr Gram.Entry.e
   end
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 71ae943792..254a789c08 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -147,7 +147,6 @@ let rec pr_raw_generic prc prlc prtac prref (x:(Genarg.rlevel, Tacexpr.raw_tacti
       pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
   | RedExprArgType ->
       pr_arg (pr_red_expr (prc,prlc,prref)) (out_gen rawwit_red_expr x)
-  | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (rawwit_tactic n) x)
   | OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
@@ -193,7 +192,6 @@ let rec pr_glob_generic prc prlc prtac x =
       pr_arg (pr_red_expr 
         (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference)))
         (out_gen globwit_red_expr x)
-  | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (globwit_tactic n) x)
   | OpenConstrArgType b -> pr_arg prc (snd (out_gen (globwit_open_constr_gen b) x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x)
@@ -237,7 +235,6 @@ let rec pr_generic prc prlc prtac x =
   | RedExprArgType ->
       pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference)) 
         (out_gen wit_red_expr x)
-  | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (wit_tactic n) x)
   | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x)
@@ -1020,3 +1017,14 @@ let _ = Tactic_debug.set_match_pattern_printer
 let _ = Tactic_debug.set_match_rule_printer
   (fun rl ->
     pr_match_rule false (pr_glob_tactic (Global.env())) pr_constr_pattern rl)
+
+open Pcoq
+
+let pr_tac_polymorphic n _ _ prtac = prtac (n,E)
+
+let _ = for i=0 to 5 do
+  declare_extra_genarg_pprule
+  (rawwit_tactic i, pr_tac_polymorphic i)
+  (globwit_tactic i, pr_tac_polymorphic i)
+  (wit_tactic i, pr_tac_polymorphic i)
+done
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 2cc30f5edd..7475754c3b 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -182,7 +182,6 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
   | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
   | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
-  | Genarg.TacticArgType n -> <:expr< Genarg.TacticArgType $mlexpr_of_int n$ >>
   | Genarg.SortArgType -> <:expr< Genarg.SortArgType >>
   | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
   | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 4601b0db41..20cf99b1bc 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -36,8 +36,6 @@ let rec make_when loc = function
       <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >>
   | _::l -> make_when loc l
 
-let is_tactic_arg = function TacticArgType _ -> true | _ -> false
-
 let rec make_let e = function
   | [] -> e
   | TacNonTerm(loc,t,_,Some p)::l ->
@@ -47,7 +45,7 @@ let rec make_let e = function
       let v = 
         (* Special case for tactics which must be stored in algebraic
            form to avoid marshalling closures and to be reprinted *)
-        if is_tactic_arg t then
+        if Pcoq.is_tactic_genarg t then
           <:expr< ($v$, Tacinterp.eval_tactic $v$) >>
         else v in
       <:expr< let $lid:p$ = $v$ in $e$ >>
@@ -84,7 +82,7 @@ let rec make_args = function
 
 let rec make_eval_tactic e = function
   | [] -> e
-  | TacNonTerm(loc,TacticArgType _,_,Some p)::l ->
+  | TacNonTerm(loc,tag,_,Some p)::l when Pcoq.is_tactic_genarg tag ->
       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