Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux niveaux syntaxiques des tacticielles

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

13 files changed, 152 insertions, 95 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 061efa49e..c0207f077 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -31,7 +31,7 @@ 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 -> <:expr< Genarg.rawwit_tactic >>
+  | 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 >>
@@ -57,7 +57,7 @@ let rec make_globwit loc = function
   | SortArgType -> <:expr< Genarg.globwit_sort >>
   | ConstrArgType -> <:expr< Genarg.globwit_constr >>
   | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >>
-  | TacticArgType -> <:expr< Genarg.globwit_tactic >>
+  | 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 >>
@@ -83,7 +83,7 @@ let rec make_wit loc = function
   | SortArgType -> <:expr< Genarg.wit_sort >>
   | ConstrArgType -> <:expr< Genarg.wit_constr >>
   | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
-  | TacticArgType -> <:expr< Genarg.wit_tactic >>
+  | 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 >>
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index cee0a1ea9..54e069512 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -27,8 +27,9 @@ type all_grammar_command =
   | Notation of (precedence * tolerability list) * notation_grammar
   | Grammar of grammar_command
   | TacticGrammar of
-      (string * (string * grammar_production list) * 
-      (Names.dir_path * Tacexpr.glob_tactic_expr))
+      int *
+      (string * grammar_production list * 
+       (Names.dir_path * Tacexpr.glob_tactic_expr))
       list
 
 val extend_grammar : all_grammar_command -> unit
@@ -39,21 +40,18 @@ type grammar_tactic_production =
   | TacNonTerm of loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option
 
 val extend_tactic_grammar :
-  string -> (string * grammar_tactic_production list) list -> unit
+  string -> grammar_tactic_production list list -> unit
 
 val extend_vernac_command_grammar :
-  string -> (string * grammar_tactic_production list) list -> unit
+  string -> grammar_tactic_production list list -> unit
 
 val get_extend_tactic_grammars :
- unit -> (string * (string * grammar_tactic_production list) list) list
+ unit -> (string * grammar_tactic_production list list) list
 val get_extend_vernac_grammars :
- unit -> (string * (string * grammar_tactic_production list) list) list
+ unit -> (string * grammar_tactic_production list list) list
 val reset_extend_grammars_v8 : unit -> unit
 
-val subst_all_grammar_command :
-  substitution -> all_grammar_command -> all_grammar_command
-
-val interp_entry_name : string -> string -> 
+val interp_entry_name : int -> string -> string -> 
   entry_type * Token.t Gramext.g_symbol
 
 val recover_notation_grammar :
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 648bb2829..097f38f01 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -246,17 +246,25 @@ GEXTEND Gram
   GLOBAL: syntax;
 
   univ:
-  [ [ univ = IDENT ->
+    [ [ univ = IDENT ->
         set_default_action_parser (parser_type_from_name univ); univ ] ]
   ;
+  grammar_tactic_level:
+    [ [ IDENT "simple_tactic" -> 0 
+      | IDENT "tactic1" -> 1
+      | IDENT "tactic2" -> 2
+      | IDENT "tactic3" -> 3
+      | IDENT "tactic4" -> 4
+      | IDENT "tactic5" -> 5 ] ]
+  ;
   syntax:
    [ [ IDENT "Token"; s = lstring ->
        Pp.warning "Token declarations are now useless"; VernacNop
 
-     | IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
+     | IDENT "Grammar"; IDENT "tactic"; lev = grammar_tactic_level;
         OPT [ ":"; IDENT "tactic" ]; ":=";
         OPT "|"; tl = LIST0 grammar_tactic_rule SEP "|" -> 
-	  VernacTacticGrammar tl
+	  VernacTacticGrammar (lev,tl)
 
      | IDENT "Grammar"; u = univ;
          tl = LIST1 grammar_entry SEP "with" -> 
@@ -416,8 +424,8 @@ GEXTEND Gram
      | -> None ]]
   ;
   grammar_tactic_rule:
-    [[ name = rule_name; "["; s = lstring; pil = LIST0 production_item; "]";
-       "->"; "["; t = Tactic.tactic; "]"  -> (name, (s,pil), t) ]]
+    [[ name = rule_name; "["; pil = LIST0 production_item; "]";
+       "->"; "["; t = Tactic.tactic; "]"  -> (name, pil, t) ]]
   ;
   grammar_rule:
     [[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->";
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 8defe13c1..e73682d22 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -41,10 +41,11 @@ let arg_of_expr = function
 
 if !Options.v7 then
 GEXTEND Gram
-  GLOBAL: tactic Vernac_.command tactic_arg;
+  GLOBAL: tactic Vernac_.command tactic_arg 
+  tactic_expr5 tactic_expr4 tactic_expr3 tactic_expr2;
 
 (*
-  GLOBAL: tactic_atom tactic_atom0 tactic_expr input_fun;
+  GLOBAL: tactic_atom tactic_atom0  input_fun;
 *)
   input_fun:
     [ [ l = base_ident -> Some l
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 265675df8..9e0a10931 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -39,8 +39,6 @@ let arg_of_expr = function
     
 (* Tactics grammar rules *)
 
-let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
-
 if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: tactic Vernac_.command tactic_expr tactic_arg;
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index f0350946f..c21feb09e 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -693,9 +693,9 @@ GEXTEND Gram
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
            VernacNotation (local,c,Some(s,modl),None,sc)
 
-     | IDENT "Tactic"; IDENT "Notation"; s = ne_string; 
-	 pil = LIST0 production_item; ":="; t = Tactic.tactic -> 
-	   VernacTacticGrammar ["",(s,pil),t]
+     | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; 
+	 pil = LIST0 production_item; ":="; t = Tactic.tactic
+         -> VernacTacticGrammar (n,["",pil,t])
 
      | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
@@ -705,6 +705,9 @@ GEXTEND Gram
         to factorize with other "Print"-based vernac entries *)
   ] ]
   ;
+  tactic_level:
+    [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ]
+  ;
   locality:
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index cc7bb3dad..135a9f8d1 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -52,7 +52,7 @@ let grammar_delete e rls =
        List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
     (List.rev rls)
 
-(* grammar_object is the superclass of all grammar entry *)
+(* grammar_object is the superclass of all grammar entries *)
 module type Gramobj =
 sig
   type grammar_object
@@ -390,10 +390,20 @@ module Tactic =
 
     (* Main entries for ltac *)
     let tactic_arg = Gram.Entry.create "tactic:tactic_arg"
-    let tactic = make_gen_entry utactic rawwit_tactic "tactic"
+    (* For v8: *)
+    let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
+    (* For v7: *)
+    let tactic_expr2 = Gram.Entry.create "tactic:tactic_expr2"
+    let tactic_expr3 = Gram.Entry.create "tactic:tactic_expr3"
+    let tactic_expr4 = Gram.Entry.create "tactic:tactic_expr4"
+    let tactic_expr5 = Gram.Entry.create "tactic:tactic_expr5"
+
+    let tactic_main_level = 5
+    let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic"
 
     (* Main entry for quotations *)
     let tactic_eoi = eoi_entry tactic
+
   end
 
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 2fdb91254..c073a3d9f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -25,7 +25,10 @@ val lexer : Token.lexer
 
 module Gram : Grammar.S with type te = Token.t
 
+(* The superclass of all grammar entries *)
 type grammar_object
+
+(* The type of typed grammar objects *)
 type typed_entry
 
 val type_of_typed_entry : typed_entry -> Extend.entry_type
@@ -39,7 +42,7 @@ val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
   bool -> constr_production_entry -> Token.t Gramext.g_symbol
 
 val grammar_extend :
-  'a Gram.Entry.e -> Gramext.position option ->
+  grammar_object Gram.Entry.e -> Gramext.position option ->
     (string option * Gramext.g_assoc option *
      (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
     -> unit
@@ -168,8 +171,16 @@ module Tactic :
     val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e
     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
+
+    (* For v7 *)
+    val tactic_expr2 : raw_tactic_expr Gram.Entry.e
+    val tactic_expr3 : raw_tactic_expr Gram.Entry.e
+    val tactic_expr4 : raw_tactic_expr Gram.Entry.e
+    val tactic_expr5 : raw_tactic_expr Gram.Entry.e
   end
 
 module Vernac_ :
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 8e409a086..0dc646198 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -19,6 +19,7 @@ open Topconstr
 open Genarg
 open Libnames
 open Pattern
+open Ppextend
 
 let pr_red_expr = Ppconstr.pr_red_expr
 let pr_may_eval = Ppconstr.pr_may_eval
@@ -42,13 +43,16 @@ let declare_extra_tactic_pprule for_v8 s (tags,prods) =
   if for_v8 then Hashtbl.add prtac_tab (s,tags) prods
 
 type 'a raw_extra_genarg_printer =
-    (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) ->
+    (constr_expr -> std_ppcmds) -> 
+    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
       'a -> std_ppcmds
 type 'a glob_extra_genarg_printer =
-    (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
+    (rawconstr_and_expr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
       'a -> std_ppcmds
 type 'a extra_genarg_printer =
-    (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
+    (Term.constr -> std_ppcmds) ->
+    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
       'a -> std_ppcmds
 
 let genarg_pprule_v7 = ref Stringmap.empty
@@ -271,7 +275,7 @@ let rec pr_raw_generic prc prlc prtac prref x =
   | RedExprArgType ->
       pr_arg (pr_red_expr 
         (prc,prref)) (out_gen rawwit_red_expr x)
-  | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic 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)
@@ -318,7 +322,7 @@ let rec pr_glob_generic prc prlc prtac x =
   | RedExprArgType ->
       pr_arg (pr_red_expr 
         (prc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x)
-  | TacticArgType -> pr_arg prtac (out_gen globwit_tactic 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)
@@ -364,7 +368,7 @@ let rec pr_generic prc prlc prtac x =
       pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x)
   | RedExprArgType ->
       pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x)
-  | TacticArgType -> pr_arg prtac (out_gen wit_tactic 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)
@@ -394,7 +398,9 @@ let rec pr_tacarg_using_rule pr_gen = function
   | [], [] -> mt ()
   | _ -> failwith "Inconsistent arguments of extended tactic"
 
-let pr_extend_gen prgen s l =
+let surround p = hov 1 (str"(" ++ p ++ str")")
+
+let pr_extend_gen prgen lev s l =
   let tab = 
     if Options.do_translate() or not !Options.v7 then prtac_tab
     else prtac_tab_v7
@@ -407,12 +413,13 @@ let pr_extend_gen prgen s l =
       if Options.do_translate() & n > 2 & String.sub s (n-2) 2 = "v7"
       then String.sub s 0 (n-2) ^ "v8"
       else s in
-    let (s,pl) = Hashtbl.find tab (s,tags) in
-    str s ++ pr_tacarg_using_rule prgen (pl,l)
+    let (lev',pl) = Hashtbl.find tab (s,tags) in
+    let p = pr_tacarg_using_rule prgen (pl,l) in
+    if lev' > lev then surround p else p
   with Not_found ->
     str s ++ prlist prgen l ++ str " (* Generic printer *)"
 
-let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) =
+let make_pr_tac (pr_tac_level,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) =
 
 let pr_bindings = pr_bindings pr_constr pr_constr in
 let pr_bindings_no_with = pr_bindings_no_with pr_constr pr_constr in
@@ -436,9 +443,9 @@ let rec pr_atom0 = function
 
   (* Main tactic printer *)
 and pr_atom1 = function
-  | TacExtend (_,s,l) -> pr_extend pr_constr pr_constr pr_tac s l
+  | TacExtend (_,s,l) -> pr_extend pr_constr pr_constr pr_tac_level 1 s l
   | TacAlias (_,s,l,_) ->
-      pr_extend pr_constr pr_constr pr_tac s (List.map snd l)
+      pr_extend pr_constr pr_constr pr_tac_level 1 s (List.map snd l)
 
   (* Basic tactics *)
   | TacIntroPattern [] as t -> pr_atom0 t
@@ -569,7 +576,7 @@ and pr_atom1 = function
   | TacRight l -> hov 1 (str "Right" ++ pr_bindings l)
   | TacSplit (_,l) -> hov 1 (str "Split" ++ pr_bindings l)
   | TacAnyConstructor (Some t) ->
-      hov 1 (str "Constructor" ++ pr_arg pr_tac0 t)
+      hov 1 (str "Constructor" ++ pr_arg (pr_tac_level (0,E)) t)
   | TacAnyConstructor None as t -> pr_atom0 t
   | TacConstructor (n,l) ->
       hov 1 (str "Constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings l)
@@ -628,6 +635,8 @@ and pr1 = function
 and pr2 = function
   | TacOrelse (t1,t2) ->
       hov 1 (pr1 t1 ++ str " Orelse" ++ brk (1,1) ++ pr3 t2)
+  | TacAtom (_,TacAlias (_,s,l,_)) ->
+      pr_extend pr_constr pr_constr pr_tac_level 2 s (List.map snd l)
   | t -> pr1 t
 
   (* Non closed prefix tactic expressions *)
@@ -637,9 +646,13 @@ and pr3 = function
   | TacRepeat t -> hov 1 (str "Repeat" ++ spc () ++ pr3 t)
   | TacProgress t -> hov 1 (str "Progress" ++ spc () ++ pr3 t)
   | TacInfo t -> hov 1 (str "Info" ++ spc () ++ pr3 t)
+  | TacAtom (_,TacAlias (_,s,l,_)) ->
+      pr_extend pr_constr pr_constr pr_tac_level 3 s (List.map snd l)
   | t -> pr2 t
 
 and pr4 = function
+  | TacAtom (_,TacAlias (_,s,l,_)) ->
+      pr_extend pr_constr pr_constr pr_tac_level 4 s (List.map snd l)
   | t -> pr3 t
 
   (* THEN and THENS tactic expressions (printed as if parsed
@@ -649,6 +662,8 @@ and pr5 = function
       hov 1 (pr5 t ++ str ";" ++ spc () ++ pr_tactic_seq_body tl)
   | TacThen (t1,t2) ->
       hov 1 (pr5 t1 ++ str ";" ++ spc () ++ pr4 t2)
+  | TacAtom (_,TacAlias (_,s,l,_)) ->
+      pr_extend pr_constr pr_constr pr_tac_level 5 s (List.map snd l)
   | t -> pr4 t
 
   (* Ltac tactic expressions *)
@@ -714,14 +729,26 @@ and pr_tacarg0 = function
 and pr_tacarg1 = function
   | TacCall (_,f,l) ->
       hov 0 (pr_ref f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l)
-  | Tacexp t -> pr_tac t
+  | Tacexp t -> pr_tac_level (6,E) t
   | t -> pr_tacarg0 t
 
 and pr_tacarg x = pr_tacarg1 x
 
 and prtac x = pr6 x
 
-in (prtac,pr0,pr_match_rule false pr_pat pr_tac)
+and prtac_level (n,p) =
+  let n = match p with E -> n | L -> n-1 | Prec n -> n | Any -> 6 in
+  match n with
+  | 0 -> pr0
+  | 1 -> pr1
+  | 2 -> pr2
+  | 3 -> pr3
+  | 4 -> pr4
+  | 5 -> pr5
+  | 6 -> pr6
+  | _ -> anomaly "Unknown tactic level"
+
+in (prtac_level,pr_match_rule false pr_pat (pr_tac_level (6,E)))
 
 let pr_raw_extend prc prlc prtac = 
   pr_extend_gen (pr_raw_generic prc prlc prtac Ppconstrnew.pr_reference)
@@ -733,8 +760,7 @@ let pr_extend prc prlc prtac =
 let pr_and_constr_expr pr (c,_) = pr c
 
 let rec glob_printers =
-    (pr_glob_tactic, 
-     pr_glob_tactic0,
+    (pr_glob_tactic_level, 
      pr_and_constr_expr Printer.pr_rawterm,
      Printer.pr_pattern,
      pr_or_var (pr_and_short_name pr_evaluable_reference),
@@ -743,16 +769,15 @@ let rec glob_printers =
      pr_located pr_id,
      pr_glob_extend)
 
-and pr_glob_tactic (t:glob_tactic_expr) = pi1 (make_pr_tac glob_printers) t
+and pr_glob_tactic_level n (t:glob_tactic_expr) =
+  fst (make_pr_tac glob_printers) n t
 
-and pr_glob_tactic0 t = pi2 (make_pr_tac glob_printers) t
+and pr_glob_match_context t =
+  snd (make_pr_tac glob_printers) t
 
-and pr_glob_match_context t = pi3 (make_pr_tac glob_printers) t
-
-let (pr_tactic,_,_) =
+let (pr_tactic_level,_) =
   make_pr_tac
-    (pr_glob_tactic,
-     pr_glob_tactic0,
+    (pr_glob_tactic_level,
      Printer.prterm,
      Printer.pr_pattern,
      pr_evaluable_reference,
@@ -760,3 +785,6 @@ let (pr_tactic,_,_) =
      pr_ltac_constant,
      pr_id,
      pr_extend)
+
+let pr_glob_tactic = pr_glob_tactic_level (6,E)
+let pr_tactic = pr_tactic_level (6,E)
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 532664274..3738c57bb 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -15,6 +15,7 @@ open Pretyping
 open Proof_type
 open Topconstr
 open Rawterm
+open Ppextend
 
 val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
 val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds
@@ -22,15 +23,15 @@ val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
 val pr_located : ('a -> std_ppcmds) -> 'a Util.located -> std_ppcmds
 
 type 'a raw_extra_genarg_printer =
-    (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) ->
+    (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) ->
       'a -> std_ppcmds
 
 type 'a glob_extra_genarg_printer =
-    (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
+    (rawconstr_and_expr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) ->
       'a -> std_ppcmds
 
 type 'a extra_genarg_printer =
-    (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) ->
+    (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) ->
       'a -> std_ppcmds
 
   (* if the boolean is false then the extension applies only to old syntax *)
@@ -44,7 +45,7 @@ type grammar_terminals = string option list
 
   (* if the boolean is false then the extension applies only to old syntax *)
 val declare_extra_tactic_pprule : bool -> string -> 
-  argument_type list * (string * grammar_terminals) -> unit
+  argument_type list * (int * grammar_terminals) -> unit
 
 val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
 
@@ -58,27 +59,28 @@ val pr_tactic : Proof_type.tactic_expr -> std_ppcmds
 val pr_glob_generic:
   (rawconstr_and_expr -> std_ppcmds) -> 
   (rawconstr_and_expr -> std_ppcmds) -> 
-  (glob_tactic_expr -> std_ppcmds) ->
+  (tolerability -> glob_tactic_expr -> std_ppcmds) ->
     glob_generic_argument -> std_ppcmds
 
 val pr_raw_generic : 
   (constr_expr -> std_ppcmds) ->
   (constr_expr -> std_ppcmds) ->
-  (raw_tactic_expr -> std_ppcmds) ->
+  (tolerability -> raw_tactic_expr -> std_ppcmds) ->
   (Libnames.reference -> std_ppcmds) ->
     (constr_expr, raw_tactic_expr) generic_argument ->
       std_ppcmds
 
 val pr_raw_extend:
   (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
-  (raw_tactic_expr -> std_ppcmds) -> string ->
-    raw_generic_argument list -> std_ppcmds
+  (tolerability -> raw_tactic_expr -> std_ppcmds) -> int ->
+    string -> raw_generic_argument list -> std_ppcmds
 
 val pr_glob_extend:
   (rawconstr_and_expr -> std_ppcmds) -> (rawconstr_and_expr -> std_ppcmds) ->
-  (glob_tactic_expr -> std_ppcmds) -> string ->
-    glob_generic_argument list -> std_ppcmds
+  (tolerability -> glob_tactic_expr -> std_ppcmds) -> int ->
+    string -> glob_generic_argument list -> std_ppcmds
 
 val pr_extend :
   (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) ->
-  (glob_tactic_expr -> std_ppcmds) -> string -> closed_generic_argument list -> std_ppcmds
+  (tolerability -> glob_tactic_expr -> std_ppcmds) -> int ->
+    string -> closed_generic_argument list -> std_ppcmds
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index d963d9450..9a5e43feb 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -275,7 +275,7 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
   | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
   | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
-  | Genarg.TacticArgType -> <:expr< Genarg.TacticArgType >>
+  | 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 dac09e8a8..3a20aad1b 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -36,6 +36,8 @@ 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 ->
@@ -45,13 +47,13 @@ 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 t = TacticArgType then
+        if is_tactic_arg t then
           <:expr< ($v$, Tacinterp.eval_tactic $v$) >>
         else v in
       <:expr< let $lid:p$ = $v$ in $e$ >>
   | _::l -> make_let e l
 
-let add_clause s (_,pt,e) l =
+let add_clause s (pt,e) l =
   let p = make_patt pt in
   let w = Some (make_when (MLast.loc_of_expr e) pt) in
   (p, w, make_let e pt)::l
@@ -62,7 +64,7 @@ let rec extract_signature = function
   | _::l -> extract_signature l
 
 let check_unicity s l =
-  let l' = List.map (fun (_,l,_) -> extract_signature l) l in
+  let l' = List.map (fun (l,_) -> extract_signature l) l in
   if not (Util.list_distinct l') then
     Pp.warning_with Pp_control.err_ft
       ("Two distinct rules of tactic entry "^s^" have the same\n"^
@@ -82,7 +84,7 @@ let rec make_args = function
 
 let rec make_eval_tactic e = function
   | [] -> e
-  | TacNonTerm(loc,TacticArgType,_,Some p)::l ->
+  | TacNonTerm(loc,TacticArgType _,_,Some p)::l ->
       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
@@ -106,11 +108,8 @@ let mlexpr_terminals_of_grammar_production = function
   | TacTerm s -> <:expr< Some $mlexpr_of_string s$ >>
   | TacNonTerm (loc,nt,g,sopt) -> <:expr< None >>
 
-let mlexpr_of_semi_clause =
-  mlexpr_of_pair mlexpr_of_string (mlexpr_of_list mlexpr_of_grammar_production)
-
 let mlexpr_of_clause =
-  mlexpr_of_list (fun (a,b,c) -> mlexpr_of_semi_clause (a,b))
+  mlexpr_of_list (fun (a,b) -> mlexpr_of_list mlexpr_of_grammar_production a)
 
 let rec make_tags loc = function
   | [] -> <:expr< [] >>
@@ -121,19 +120,20 @@ let rec make_tags loc = function
       <:expr< [ $t$ :: $l$ ] >>
   | _::l -> make_tags loc l
 
-let make_one_printing_rule (s,pt,e) =
+let make_one_printing_rule (pt,e) =
+  let level = mlexpr_of_int 0 in (* only level 0 supported here *)
   let loc = MLast.loc_of_expr e in
   let prods = mlexpr_of_list mlexpr_terminals_of_grammar_production pt in
-  <:expr< ($make_tags loc pt$, ($str:s$, $prods$)) >>
+  <:expr< ($make_tags loc pt$, ($level$, $prods$)) >>
 
 let make_printing_rule = mlexpr_of_list make_one_printing_rule
 
 let new_tac_ext (s,cl) =
   (String.lowercase s, List.map 
-    (fun (s,l,e) ->
-      (String.lowercase s, List.map
-        (function TacTerm s -> TacTerm (String.lowercase s)
-          | t -> t) l,
+    (fun (l,e) ->
+      (List.map (function 
+	| TacTerm s -> TacTerm (String.lowercase s)
+        | t -> t) l,
         e))
     cl)
 
@@ -167,11 +167,13 @@ let rec contains_epsilon = function
   | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2
   | ExtraArgType("hintbases") -> true
   | _ -> false
-let is_atomic =
-  List.for_all
-    (function
-        TacTerm _ -> false
-      | TacNonTerm(_,t,_,_) -> contains_epsilon t)
+let is_atomic = function
+  | TacTerm s :: l when 
+      List.for_all (function
+          TacTerm _ -> false
+	| TacNonTerm(_,t,_,_) -> contains_epsilon t) l
+	-> [s]
+  | _ -> []
 
 let declare_tactic loc s cl =
   let (s',cl') = new_tac_ext (s,cl) in
@@ -180,7 +182,7 @@ let declare_tactic loc s cl =
   let se' = mlexpr_of_string s' in
   let pp = make_printing_rule cl in
   let gl = mlexpr_of_clause cl in
-  let hide_tac (_,p,e) =
+  let hide_tac (p,e) =
     (* reste a definir les fonctions cachees avec des noms frais *)
     let stac = "h_"^s' in
     let e = 
@@ -194,8 +196,8 @@ let declare_tactic loc s cl =
   let hidden = if List.length cl = 1 then List.map hide_tac cl' else [] in
   let se = mlexpr_of_string s in
   let atomic_tactics =
-    mlexpr_of_list (fun (s,_,_) -> mlexpr_of_string s)
-      (List.filter (fun (_,al,_) -> is_atomic al) cl') in
+    mlexpr_of_list mlexpr_of_string
+      (List.flatten (List.map (fun (al,_) -> is_atomic al) cl')) in
   <:str_item<
     declare
       open Pcoq;
@@ -265,10 +267,8 @@ EXTEND
          declare_tactic_v7 loc s l ] ]
   ;
   tacrule:
-    [ [ "["; s = STRING; l = LIST0 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]"
-        ->
-       if s = "" then Util.user_err_loc (loc,"",Pp.str "Tactic name is empty");
-       (s,l,e)
+    [ [ "["; l = LIST0 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]"
+        -> (l,e)
     ] ]
   ;
   tacargs:
@@ -276,6 +276,7 @@ EXTEND
         let t, g = interp_entry_name loc e in
         TacNonTerm (loc, t, g, Some s)
       | s = STRING ->
+	if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal");
         TacTerm s
     ] ]
   ;
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 33148ecea..6e2f5fe3a 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -81,11 +81,8 @@ let mlexpr_of_grammar_production = function
 
 let mlexpr_of_clause =
   mlexpr_of_list
-    (fun (a,b,c) ->
-      (mlexpr_of_pair
-	mlexpr_of_string
-	(mlexpr_of_list mlexpr_of_grammar_production)
-	(a,b)))
+    (fun (a,b,c) -> 
+      mlexpr_of_list mlexpr_of_grammar_production (VernacTerm a::b))
 
 let declare_command loc s cl =
   let gl = mlexpr_of_clause cl in