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

13 files changed, 155 insertions, 71 deletions

diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index 56abfb82b..e1b8e7125 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -239,9 +239,9 @@ and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tacti
    by the list of integers given as extra arguments.
  *)
 
-let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level
-let globwit_main_tactic = globwit_tactic Pcoq.Tactic.tactic_main_level
-let wit_main_tactic = wit_tactic Pcoq.Tactic.tactic_main_level
+let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level
+let globwit_main_tactic = Pcoq.globwit_tactic Pcoq.tactic_main_level
+let wit_main_tactic = Pcoq.wit_tactic Pcoq.tactic_main_level
 
 
 let on_then = function [t1;t2;l] ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 585e4bfb6..ecb04e075 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -682,7 +682,7 @@ let xlate_with_names = function
     IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
   | fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
 
-let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level
+let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level
 
 let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
   function
@@ -1271,14 +1271,15 @@ and coerce_genarg_to_TARG x =
       (CT_coerce_FORMULA_to_SCOMMENT_CONTENT (xlate_formula (out_gen rawwit_constr x)))
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
   | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
-  | TacticArgType n ->
-      let t = xlate_tactic (out_gen (rawwit_tactic n) x) in
-      CT_coerce_TACTIC_COM_to_TARG t
   | OpenConstrArgType b -> 
       CT_coerce_SCOMMENT_CONTENT_to_TARG
       	(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
 					 (snd (out_gen
 					    (rawwit_open_constr_gen b) x))))
+  | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
+      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
+      CT_coerce_TACTIC_COM_to_TARG t
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
   | BindingsArgType -> xlate_error "TODO: generic with bindings"
   | RedExprArgType -> xlate_error "TODO: generic red expr"
@@ -1368,8 +1369,9 @@ let coerce_genarg_to_VARG x =
       (CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula (out_gen rawwit_constr x)))
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
   | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
-  | TacticArgType n ->
-      let t = xlate_tactic (out_gen (rawwit_tactic n) x) in
+  | ExtraArgType s as y when Pcoq.is_tactic_genarg y ->
+      let n = out_some (Pcoq.tactic_genarg_level s) in
+      let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in
       CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
   | OpenConstrArgType _ -> xlate_error "TODO: generic open constr"
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 294678d48..e5713a6e2 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -33,7 +33,6 @@ type argument_type =
   | ConstrArgType
   | ConstrMayEvalArgType
   | QuantHypArgType
-  | TacticArgType of int
   | OpenConstrArgType of bool
   | ConstrWithBindingsArgType
   | BindingsArgType
@@ -145,10 +144,6 @@ let rawwit_constr_may_eval = ConstrMayEvalArgType
 let globwit_constr_may_eval = ConstrMayEvalArgType
 let wit_constr_may_eval = ConstrMayEvalArgType
 
-let rawwit_tactic n = TacticArgType n
-let globwit_tactic n = TacticArgType n
-let wit_tactic n = TacticArgType n
-
 let rawwit_open_constr_gen b = OpenConstrArgType b
 let globwit_open_constr_gen b = OpenConstrArgType b 
 let wit_open_constr_gen b = OpenConstrArgType b
diff --git a/interp/genarg.mli b/interp/genarg.mli
index f82eac0cb..3f96baae8 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -72,7 +72,6 @@ RefArgType                     reference                global_reference
 ConstrArgType                  constr_expr              constr
 ConstrMayEvalArgType           constr_expr may_eval     constr
 QuantHypArgType                quantified_hypothesis    quantified_hypothesis
-TacticArgType                  raw_tactic_expr          tactic
 OpenConstrArgType              constr_expr              open_constr
 ConstrBindingsArgType      constr_expr with_bindings constr with_bindings
 List0ArgType of argument_type
@@ -171,11 +170,6 @@ val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,rlevel,'ta) abstract
 val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel,'ta) abstract_argument_type
 val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel,'ta) abstract_argument_type
 
-(* TODO: transformer tactic en extra arg *)
-val rawwit_tactic : int -> ('ta,rlevel,'ta) abstract_argument_type
-val globwit_tactic : int -> ('ta,glevel,'ta) abstract_argument_type
-val wit_tactic : int -> ('ta,tlevel,'ta) abstract_argument_type
-
 val wit_list0 :
   ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
 
@@ -249,7 +243,6 @@ type argument_type =
   | ConstrArgType
   | ConstrMayEvalArgType
   | QuantHypArgType
-  | TacticArgType of int
   | OpenConstrArgType of bool
   | ConstrWithBindingsArgType
   | BindingsArgType
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index d1f82c1d9..a4239713b 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 f7127ea61..bc351cbaa 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 cb45a9f45..5c6216687 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 690810d8a..404f3ab90 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 71ae94379..254a789c0 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 2cc30f5ed..7475754c3 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 4601b0db4..20cf99b1b 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
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a6155598c..521bf5409 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -37,54 +37,41 @@ let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings)
 *)
 
 (* Julien: Mise en commun des differentes version de replace with in by 
-   TODO: améliorer l'affichage et deplacer dans extraargs
+   TODO: deplacer dans extraargs
 
 *)
 
-
-let pr_by_arg_tac prc _ _ opt_c = 
+let pr_by_arg_tac _prc _prlc prtac opt_c = 
   match opt_c with 
     | None -> mt ()
-    | Some c -> spc () ++ hov 2 (str "by" ++ spc ()  )
+    | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
 
 (* Julien Forest: on voudrait pouvoir passer la loc mais je 
 n'ai pas reussi 
 *)
 
-let pr_in_arg_hyp  = 
-fun prc _ _ opt_c->
+let pr_in_arg_hyp _prc _prlc _prtac opt_c =
   match opt_c with 
     | None -> mt ()
-    | Some c -> 
-	spc () ++ hov 2 (str "by" ++ spc () ++ 
-			   Pptactic.pr_or_var (fun _ -> mt ()) 
-			   (Rawterm.ArgVar(Util.dummy_loc,c))
-			)
-
-
-
+    | Some id -> spc () ++ hov 2 (str "by" ++ spc () ++ Nameops.pr_id id)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
   PRINTED BY pr_by_arg_tac
-| [ "by" tactic(c) ] -> [ Some c ]
+| [ "by" tactic3(c) ] -> [ Some c ]
 | [ ] -> [ None ]
 END
  
 ARGUMENT EXTEND in_arg_hyp
   TYPED AS ident_opt
   PRINTED BY pr_in_arg_hyp
-| [ "in" int_or_var(c) ] -> 
-    [ match c with
-	| Rawterm.ArgVar(_,c) ->  Some (c)
-	| _ -> Util.error "in must be used with an identifier" 
-    ]
+| [ "in" ident(c) ] -> [ Some (c) ]
 | [ ] -> [ None ]
 END
 
 TACTIC EXTEND replace 
-| ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp)  by_arg_tac(tac)  ] ->
-    [ new_replace c1 c2 in_hyp (Util.option_map Tacinterp.eval_tactic tac)  ]
+   ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ]
+-> [ new_replace c1 c2 in_hyp (Util.option_map Tacinterp.eval_tactic tac) ]
 END
 
 (* Julien:
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 20ca5dc93..fef9ba95a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -46,6 +46,7 @@ open Inductiveops
 open Syntax_def
 open Pretyping
 open Pretyping.Default
+open Pcoq
 
 let error_syntactic_metavariables_not_allowed loc =
   user_err_loc 
@@ -867,9 +868,6 @@ and intern_genarg ist x =
         (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
   | RedExprArgType ->
       in_gen globwit_red_expr (intern_redexp ist (out_gen rawwit_red_expr x))
-  | TacticArgType n ->
-      in_gen (globwit_tactic n) (intern_tactic ist
-	(out_gen (rawwit_tactic n) x))
   | OpenConstrArgType b ->
       in_gen (globwit_open_constr_gen b)
         ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x)))
@@ -883,7 +881,14 @@ and intern_genarg ist x =
   | List1ArgType _ -> app_list1 (intern_genarg ist) x
   | OptArgType _ -> app_opt (intern_genarg ist) x
   | PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x
-  | ExtraArgType s -> lookup_genarg_glob s ist x
+  | ExtraArgType s ->
+      match tactic_genarg_level s with
+      | Some n -> 
+          (* Special treatment of tactic arguments *)
+          in_gen (globwit_tactic n) (intern_tactic ist
+	    (out_gen (rawwit_tactic n) x))
+      | None ->
+          lookup_genarg_glob s ist x
 
 (************* End globalization ************)
 
@@ -1659,7 +1664,6 @@ and interp_genarg ist goal x =
           (out_gen globwit_quant_hyp x))
   | RedExprArgType ->
       in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x))
-  | TacticArgType n -> in_gen (wit_tactic n) (out_gen (globwit_tactic n) x)
   | OpenConstrArgType casted ->
       in_gen (wit_open_constr_gen casted) 
         (pf_interp_open_constr casted ist goal 
@@ -1674,7 +1678,13 @@ and interp_genarg ist goal x =
   | List1ArgType _ -> app_list1 (interp_genarg ist goal) x
   | OptArgType _ -> app_opt (interp_genarg ist goal) x
   | PairArgType _ -> app_pair (interp_genarg ist goal) (interp_genarg ist goal) x
-  | ExtraArgType s -> lookup_interp_genarg s ist goal x
+  | ExtraArgType s -> 
+      match tactic_genarg_level s with
+      | Some n -> 
+          (* Special treatment of tactic arguments *)
+          in_gen (wit_tactic n) (out_gen (globwit_tactic n) x)
+      | None -> 
+          lookup_interp_genarg s ist goal x
 
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
@@ -1879,13 +1889,17 @@ and interp_atomic ist gl = function
     | ConstrMayEvalArgType ->
 	VConstr
           (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
-    | TacticArgType n -> 
-	val_interp ist gl (out_gen (globwit_tactic n) x)
+    | ExtraArgType s when tactic_genarg_level s <> None ->
+          (* Special treatment of tactic arguments *)
+	val_interp ist gl 
+          (out_gen (globwit_tactic (out_some (tactic_genarg_level s))) x)
     | StringArgType | BoolArgType
     | QuantHypArgType | RedExprArgType 
-    | OpenConstrArgType _ | ConstrWithBindingsArgType | BindingsArgType 
-    | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
+    | OpenConstrArgType _ | ConstrWithBindingsArgType 
+    | ExtraArgType _ | BindingsArgType 
+    | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
 	-> error "This generic type is not supported in alias"
+        
     in
     let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in
     let v = locate_tactic_call loc (val_interp { ist with lfun=lfun } gl body)
@@ -2184,9 +2198,6 @@ and subst_genarg subst (x:glob_generic_argument) =
           (out_gen globwit_quant_hyp x))
   | RedExprArgType ->
       in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
-  | TacticArgType n ->
-      in_gen (globwit_tactic n)
-        (subst_tactic subst (out_gen (globwit_tactic n) x))
   | OpenConstrArgType b ->
       in_gen (globwit_open_constr_gen b)
         ((),subst_rawconstr subst (snd (out_gen (globwit_open_constr_gen b) x)))
@@ -2200,7 +2211,14 @@ and subst_genarg subst (x:glob_generic_argument) =
   | List1ArgType _ -> app_list1 (subst_genarg subst) x
   | OptArgType _ -> app_opt (subst_genarg subst) x
   | PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x
-  | ExtraArgType s -> lookup_genarg_subst s subst x
+  | ExtraArgType s ->
+      match tactic_genarg_level s with
+      | Some n -> 
+          (* Special treatment of tactic arguments *)
+          in_gen (globwit_tactic n)
+            (subst_tactic subst (out_gen (globwit_tactic n) x))
+      | None -> 
+          lookup_genarg_subst s subst x
 
 (***************************************************************************)
 (* Tactic registration *)