Rationalizing the use of the various EXTEND macros.

Those macros used to handle in a special way the grammar entries and generic
arguments known statically from Coq, i.e. defined before Pcoq. This was hardly
predictible and very implementation-dependent.

We made the EXTEND macros much more light-weight by treating in a uniform way
all entries and arguments. Now, they are all produced by outputing the name
as-is for entries and as "wit_$name" for genargs, thus letting the scope
of the ML code decide which entrie is going to be taken. This is documented
in the dev/ changelog.

This also allows to get rid of a lot of dependencies in the grammar preprocessor,
reducing it to a small functional shell. It is still depending on Compat, but it
is most probably possible to reduce the code size even more.

35 files changed, 321 insertions, 190 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 0581a5f85..1f5ba7862 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -66,6 +66,15 @@
     Context.Named.t = LocalAssum of Names.Id.t * Constr.t
 	            | LocalDef of Names.Id.t * Constr.t * Constr.t
 
+- The various EXTEND macros do not handle specially the Coq-defined entries
+  anymore. Instead, they just output a name that have to exist in the scope
+  of the ML code. The parsing rules (VERNAC) ARGUMENT EXTEND will look for
+  variables "$name" of type Gram.entry, while the parsing rules of
+  (VERNAC COMMAND | TACTIC) EXTEND, as well as the various TYPED AS clauses will
+  look for variables "wit_$name" of type Genarg.genarg_type. The small DSL
+  for constructing compound entries still works over this scheme. Note that in
+  the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound
+  in the parsing rules, so beware of recursive calls.
 
 =========================================
 = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 46c68ecc3..5bf7b65d7 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -10,10 +10,8 @@
 
 open Genarg
 open Q_util
-open Egramml
 open Compat
 open Extend
-open Pcoq
 
 let loc = CompatLoc.ghost
 let default_loc = <:expr< Loc.ghost >>
@@ -23,12 +21,7 @@ let qualified_name loc s =
   let (name, path) = CList.sep_last path in
   qualified_name loc path name
 
-let mk_extraarg loc s =
-  try
-    let name = Genarg.get_name0 s in
-    qualified_name loc name
-  with Not_found ->
-    <:expr< $lid:"wit_"^s$ >>
+let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>
 
 let rec make_wit loc = function
   | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
@@ -41,28 +34,19 @@ let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >>
 let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >>
 let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
 
-let has_extraarg l =
-  let check = function
-  | ExtNonTerminal(ExtraArgType _, _, _) -> true
-  | _ -> false
-  in
-  List.exists check l
-
 let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< (fun loc -> $act$) >>
-    | ExtNonTerminal (t, _, p) :: tl ->
-	<:expr<
-            (fun $lid:p$ ->
-               let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$)
-        >>
+    | ExtNonTerminal (_, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
     | ExtTerminal _ :: tl ->
 	<:expr< (fun _ -> $make tl$) >> in
   make (List.rev pil)
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >>
-  | ExtNonTerminal (_, g, _) -> mlexpr_of_prod_entry_key g
+  | ExtNonTerminal (_, g, _) ->
+    let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in
+    mlexpr_of_prod_entry_key base g
 
 let rec make_prod = function
 | [] -> <:expr< Extend.Stop >>
@@ -71,6 +55,27 @@ let rec make_prod = function
 let make_rule loc (prods,act) =
   <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >>
 
+let is_ident x = function
+| <:expr< $lid:s$ >> -> CString.equal s x
+| _ -> false
+
+let make_extend loc s cl wit = match cl with
+| [[ExtNonTerminal (_, Uentry e, id)], act] when is_ident id act ->
+  (** Special handling of identity arguments by not redeclaring an entry *)
+  <:str_item<
+    value $lid:s$ =
+      let () = Pcoq.register_grammar $wit$ $lid:e$ in
+      $lid:e$
+  >>
+| _ ->
+  let se = mlexpr_of_string s in
+  let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
+  <:str_item<
+    value $lid:s$ =
+      let $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ (Genarg.rawwit $wit$) in
+      let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in
+      $lid:s$ >>
+
 let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let rawtyp, rawpr, globtyp, globpr = match typ with
     | `Uniform typ ->
@@ -136,8 +141,6 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   in
   let se = mlexpr_of_string s in
   let wit = <:expr< $lid:"wit_"^s$ >> in
-  let rawwit = <:expr< Genarg.rawwit $wit$ >> in
-  let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
   declare_str_items loc
    [ <:str_item<
       value ($lid:"wit_"^s$) =
@@ -146,10 +149,8 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
      <:str_item< Genintern.register_intern0 $wit$ $glob$ >>;
      <:str_item< Genintern.register_subst0 $wit$ $subst$ >>;
      <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>;
-     <:str_item<
-      value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
+     make_extend loc s cl wit;
      <:str_item< do {
-      Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]);
       Pptactic.declare_extra_genarg_pprule
         $wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$;
       Egramcoq.create_ltac_quotation $se$
@@ -160,8 +161,6 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
 let declare_vernac_argument loc s pr cl =
   let se = mlexpr_of_string s in
   let wit = <:expr< $lid:"wit_"^s$ >> in
-  let rawwit = <:expr< Genarg.rawwit $wit$ >> in
-  let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
   let pr_rules = match pr with
     | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >>
     | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in
@@ -169,17 +168,14 @@ let declare_vernac_argument loc s pr cl =
    [ <:str_item<
       value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) =
         Genarg.create_arg $se$ >>;
-     <:str_item<
-      value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
+     make_extend loc s cl wit;
     <:str_item< do {
-      Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]);
       Pptactic.declare_extra_genarg_pprule $wit$
         $pr_rules$
         (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer"))
         (fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) }
       >> ]
 
-open Pcoq
 open Pcaml
 open PcamlSig (* necessary for camlp4 *)
 
@@ -236,10 +232,7 @@ EXTEND
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
         ExtNonTerminal (type_of_user_symbol e, e, s)
-      | s = STRING ->
-	  if String.length s > 0 && Util.is_letter s.[0] then
-	    Lexer.add_keyword s;
-          ExtTerminal s
+      | s = STRING -> ExtTerminal s
     ] ]
   ;
   entry_name:
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 6a265bf4a..ae18925ea 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -1,46 +1,22 @@
 Coq_config
 
-Hook
-Terminal
 Hashset
 Hashcons
-CSet
 CMap
 Int
-Dyn
-HMap
 Option
 Store
 Exninfo
-Backtrace
-Pp_control
-Flags
 Loc
 CList
 CString
-Serialize
-Stateid
-Feedback
-Pp
 
-CArray
-CStack
-Util
-Ppstyle
-Errors
 Segmenttree
 Unicodetable
 Unicode
-Genarg
-
-Stdarg
-Constrarg
 
 Tok
 Compat
-Lexer
-Entry
-Pcoq
 
 Q_util
 Argextend
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 1848bf85f..4160d03c5 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -47,44 +47,63 @@ let mlexpr_of_option f = function
 let mlexpr_of_ident id =
   <:expr< Names.Id.of_string $str:id$ >>
 
-let repr_entry e =
-  let entry u =
-    let _ = Pcoq.get_entry u e in
-    Some (Entry.univ_name u, e)
-  in
-  try entry Pcoq.uprim with Not_found ->
-  try entry Pcoq.uconstr with Not_found ->
-  try entry Pcoq.utactic with Not_found -> None
-
-let rec mlexpr_of_prod_entry_key = function
-  | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >>
-  | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
-  | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >>
-  | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
-  | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >>
-  | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
-  | Extend.Uentry e ->
-    begin match repr_entry e with
-    | None -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >>
-    | Some (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >>
-    end
+let rec mlexpr_of_prod_entry_key f = function
+  | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Uentry e -> <:expr< Pcoq.Aentry $f e$ >>
   | Extend.Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
     assert (CString.equal e "tactic");
     if l = 5 then <:expr< Pcoq.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
     else <:expr< Pcoq.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
 
-let type_entry u e =
-  let Pcoq.TypedEntry (t, _) = Pcoq.get_entry u e in
-  Genarg.unquote t
-
 let rec type_of_user_symbol = function
 | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s ->
   Genarg.ListArgType (type_of_user_symbol s)
 | Uopt s ->
   Genarg.OptArgType (type_of_user_symbol s)
-| Uentry e | Uentryl (e, _) ->
-  try type_entry Pcoq.uprim e with Not_found ->
-  try type_entry Pcoq.uconstr e with Not_found ->
-  try type_entry Pcoq.utactic e with Not_found ->
-  Genarg.ExtraArgType e
+| Uentry e | Uentryl (e, _) -> Genarg.ExtraArgType e
+
+let coincide s pat off =
+  let len = String.length pat in
+  let break = ref true in
+  let i = ref 0 in
+  while !break && !i < len do
+    let c = Char.code s.[off + !i] in
+    let d = Char.code pat.[!i] in
+    break := Int.equal c d;
+    incr i
+  done;
+  !break
+
+let rec parse_user_entry s sep =
+  let l = String.length s in
+  if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
+    let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
+    Ulist1 entry
+  else if l > 12 && coincide s "ne_" 0 &&
+                   coincide s "_list_sep" (l-9) then
+    let entry = parse_user_entry (String.sub s 3 (l-12)) "" in
+    Ulist1sep (entry, sep)
+  else if l > 5 && coincide s "_list" (l-5) then
+    let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
+    Ulist0 entry
+  else if l > 9 && coincide s "_list_sep" (l-9) then
+    let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
+    Ulist0sep (entry, sep)
+  else if l > 4 && coincide s "_opt" (l-4) then
+    let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
+    Uopt entry
+  else if l > 5 && coincide s "_mods" (l-5) then
+    let entry = parse_user_entry (String.sub s 0 (l-1)) "" in
+    Umodifiers entry
+  else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
+    let n = Char.code s.[6] - 48 in
+    Uentryl ("tactic", n)
+  else
+    let s = match s with "hyp" -> "var" | _ -> s in
+    Uentry s
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 837ec6fb0..5f292baf3 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -28,6 +28,8 @@ val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
 val mlexpr_of_ident : string -> MLast.expr
 
-val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr
+val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr
 
 val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type
+
+val parse_user_entry : string -> string -> Extend.user_symbol
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index c35fa00d2..1951b8b45 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -10,14 +10,8 @@
 
 (** Implementation of the TACTIC EXTEND macro. *)
 
-open Util
-open Pp
-open Names
-open Genarg
 open Q_util
 open Argextend
-open Pcoq
-open Egramml
 open Compat
 
 let dloc = <:expr< Loc.ghost >>
@@ -39,14 +33,6 @@ let rec mlexpr_of_argtype loc = function
       <:expr< Genarg.PairArgType $t1$ $t2$ >>
   | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >>
 
-let rec make_when loc = function
-  | [] -> <:expr< True >>
-  | ExtNonTerminal (t, _, p) :: l ->
-      let l = make_when loc l in
-      let t = mlexpr_of_argtype loc t in
-      <:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >>
-  | _::l -> make_when loc l
-
 let rec make_let raw e = function
   | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
   | ExtNonTerminal (t, _, p) :: l ->
@@ -64,29 +50,21 @@ 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
-  if not (Util.List.distinct l') then
-    Pp.msg_warning
-      (strbrk ("Two distinct rules of tactic entry "^s^" have the same "^
-      "non-terminals in the same order: put them in distinct tactic entries"))
-
 let make_clause (pt,_,e) =
   (make_patt pt,
    vala None,
    make_let false e pt)
 
 let make_fun_clauses loc s l =
-  check_unicity s l;
   let map c = Compat.make_fun loc [make_clause c] in
   mlexpr_of_list map l
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
   | ExtNonTerminal (nt, g, id) ->
+    let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in
       <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
-      $mlexpr_of_prod_entry_key g$ >>
+      $mlexpr_of_prod_entry_key base g$ >>
 
 let mlexpr_of_clause cl =
   mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
@@ -125,7 +103,7 @@ let declare_tactic loc s c cl = match cl with
     (** Special handling of tactics without arguments: such tactics do not do
         a Proofview.Goal.nf_enter to compute their arguments. It matters for some
         whole-prof tactics like [shelve_unifiable]. *)
-    if List.is_empty rem then
+    if CList.is_empty rem then
       <:expr< fun _ $lid:"ist"$ -> $tac$ >>
     else
       let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
@@ -200,7 +178,7 @@ EXTEND
         let e = parse_user_entry e sep in
         ExtNonTerminal (type_of_user_symbol e, e, s)
       | s = STRING ->
-	if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
+	let () = if CString.is_empty s then failwith "Empty terminal." in
         ExtTerminal s
     ] ]
   ;
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 3bb1e0907..453907689 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -10,13 +10,9 @@
 
 (** Implementation of the VERNAC EXTEND macro. *)
 
-open Pp
-open Util
 open Q_util
 open Argextend
 open Tacextend
-open Pcoq
-open Egramml
 open Compat
 
 type rule = {
@@ -42,7 +38,7 @@ let rec make_let e = function
 
 let make_clause { r_patt = pt; r_branch = e; } =
   (make_patt pt,
-   vala (Some (make_when (MLast.loc_of_expr e) pt)),
+   vala None,
    make_let e pt)
 
 (* To avoid warnings *)
@@ -58,34 +54,34 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
   match c ,cg with
   | Some c, _ ->
      (make_patt pt,
-      vala (Some (make_when (MLast.loc_of_expr c) pt)),
+      vala None,
       make_let (mk_ignore c pt) pt)
   | None, Some cg ->
      (make_patt pt,
-      vala (Some (make_when (MLast.loc_of_expr cg) pt)),
+      vala None,
       <:expr< fun () -> $cg$ $str:s$ >>)
-  | None, None -> msg_warning
-      (strbrk("Vernac entry \""^s^"\" misses a classifier. "^
+  | None, None -> prerr_endline
+      (("Vernac entry \""^s^"\" misses a classifier. "^
          "A classifier is a function that returns an expression "^
-         "of type vernac_classification (see Vernacexpr). You can: ")++
-       str"- "++hov 0 (
-        strbrk("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^
-          "new vernacular command does not alter the system state;"))++fnl()++
-       str"- "++hov 0 (
-        strbrk("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^
+         "of type vernac_classification (see Vernacexpr). You can: ") ^
+       "- " ^ (
+        ("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^
+          "new vernacular command does not alter the system state;"))^ "\n" ^
+       "- " ^ (
+        ("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^
           "new vernacular command alters the system state but not the "^
-          "parser nor it starts a proof or ends one;"))++fnl()++
-       str"- "++hov 0 (
-        strbrk("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^
+          "parser nor it starts a proof or ends one;"))^ "\n" ^
+       "- " ^ (
+        ("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^
           "a global function f.  The function f will be called passing "^
-          "\""^s^"\" as the only argument;")) ++fnl()++
-       str"- "++hov 0 (
-        strbrk"Add a specific classifier in each clause using the syntax:"
-        ++fnl()++strbrk("'[...] => [ f ] -> [...]'. "))++fnl()++
-       strbrk("Specific classifiers have precedence over global "^
-         "classifiers. Only one classifier is called.")++fnl());
+          "\""^s^"\" as the only argument;")) ^ "\n" ^
+       "- " ^ (
+        "Add a specific classifier in each clause using the syntax:"
+        ^ "\n" ^("'[...] => [ f ] -> [...]'. "))^ "\n" ^
+       ("Specific classifiers have precedence over global "^
+         "classifiers. Only one classifier is called.") ^ "\n");
     (make_patt pt,
-      vala (Some (make_when loc pt)),
+      vala None,
       <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
 
 let make_fun_clauses loc s l =
@@ -164,8 +160,7 @@ EXTEND
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]";
         d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      if String.is_empty s then
-        Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
+      let () = if CString.is_empty s then failwith "Command name is empty." in
       let b = <:expr< fun () -> $e$ >> in
       { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
       | "[" ; "-" ; l = LIST1 args ; "]" ;
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index ead4e3969..20ee7aa4f 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -82,3 +82,13 @@ let () =
   register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp";
   register_name0 wit_bindings "Constrarg.wit_bindings";
   register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings";
+  ()
+
+(** Aliases *)
+
+let wit_reference = wit_ref
+let wit_global = wit_ref
+let wit_clause = wit_clause_dft_concl
+let wit_quantified_hypothesis = wit_quant_hyp
+let wit_intropattern = wit_intro_pattern
+let wit_redexpr = wit_red_expr
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 5c26af3c2..1197b85a2 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -72,3 +72,15 @@ val wit_red_expr :
 val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
 
 val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+
+(** Aliases for compatibility *)
+
+val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_clause :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+val wit_redexpr :
+  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 56b995e53..e497c996f 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -28,3 +28,8 @@ let () = register_name0 wit_bool "Stdarg.wit_bool"
 let () = register_name0 wit_int "Stdarg.wit_int"
 let () = register_name0 wit_string "Stdarg.wit_string"
 let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident"
+
+(** Aliases for compatibility *)
+
+let wit_integer = wit_int
+let wit_preident = wit_pre_ident
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index d8904dab8..e1f648d7f 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -19,3 +19,8 @@ val wit_int : int uniform_genarg_type
 val wit_string : string uniform_genarg_type
 
 val wit_pre_ident : string uniform_genarg_type
+
+(** Aliases for compatibility *)
+
+val wit_integer : int uniform_genarg_type
+val wit_preident : string uniform_genarg_type
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
index 13ed80464..eed6caea3 100644
--- a/parsing/highparsing.mllib
+++ b/parsing/highparsing.mllib
@@ -4,4 +4,3 @@ G_prim
 G_proofs
 G_tactic
 G_ltac
-G_obligations
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 232e9aee3..8b8b38c34 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -724,7 +724,7 @@ let strip s =
 
 let terminal s =
   let s = strip s in
-  let () = match s with "" -> Errors.error "empty token." | _ -> () in
+  let () = match s with "" -> failwith "empty token." | _ -> () in
   if is_ident_not_keyword s then IDENT s
   else if is_number s then INT s
   else KEYWORD s
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 52437e386..b769a3cbc 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -200,8 +200,6 @@ let parse_string f x =
 
 type gram_universe = Entry.universe
 
-let trace = ref false
-
 let uprim   = Entry.uprim
 let uconstr = Entry.uconstr
 let utactic = Entry.utactic
@@ -231,37 +229,35 @@ let get_typed_entry e =
 let new_entry etyp u s =
   let utab = get_utable u in
   let uname = Entry.univ_name u in
-  if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" uname s; flush stderr);
   let _ = Entry.create u s in
   let ename = uname ^ ":" ^ s in
   let e = Gram.entry_create ename in
   Hashtbl.add utab s (TypedEntry (etyp, e)); e
 
-let create_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
-  let utab = get_utable u in
-  try
-    let TypedEntry (typ, e) = Hashtbl.find utab s in
-    match abstract_argument_type_eq typ etyp with
-    | None ->
-      let u = Entry.univ_name u in
-      failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type");
-    | Some Refl -> e
-  with Not_found ->
-    new_entry etyp u s
+let make_gen_entry u rawwit s = new_entry rawwit u s
 
-let create_constr_entry s = create_entry uconstr s (rawwit wit_constr)
+module GrammarObj =
+struct
+  type ('r, _, _) obj = 'r Gram.entry
+  let name = "grammar"
+  let default _ = None
+end
 
-let create_generic_entry s wit = create_entry utactic s wit
+module Grammar = Register(GrammarObj)
 
-(* [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 *)
+let register_grammar = Grammar.register0
+let genarg_grammar = Grammar.obj
 
-let make_gen_entry u rawwit s =
-  let univ = get_utable u in
-  let uname = Entry.univ_name u in
-  let e = Gram.entry_create (uname ^ ":" ^ s) in
-  let _ = Entry.create u s in
-  Hashtbl.add univ s (TypedEntry (rawwit, e)); e
+let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
+  let utab = get_utable u in
+  if Hashtbl.mem utab s then
+    let u = Entry.univ_name u in
+    failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists");
+  else
+    let e = new_entry etyp u s in
+    let Rawwit t = etyp in
+    let () = Grammar.register0 t e in
+    e
 
 (* Initial grammar entries *)
 
@@ -312,7 +308,7 @@ module Constr =
     let operconstr = gec_constr "operconstr"
     let constr_eoi = eoi_entry constr
     let lconstr = gec_constr "lconstr"
-    let binder_constr = create_constr_entry "binder_constr"
+    let binder_constr = gec_constr "binder_constr"
     let ident = make_gen_entry uconstr (rawwit wit_ident) "ident"
     let global = make_gen_entry uconstr (rawwit wit_ref) "global"
     let sort = make_gen_entry uconstr (rawwit wit_sort) "sort"
@@ -612,7 +608,7 @@ let compute_entry allow_create adjust forpat = function
         try get_entry u n
         with Not_found when allow_create ->
           let wit = rawwit wit_constr in
-          TypedEntry (wit, create_entry u n wit)
+          TypedEntry (wit, create_generic_entry u n wit)
       in
       object_of_typed_entry e, None, true
 
@@ -860,3 +856,32 @@ let epsilon_value f e =
   let entry = G.entry_create "epsilon" in
   let () = maybe_uncurry (Gram.extend entry) ext in
   try Some (parse_string entry "") with _ -> None
+
+(** Registering grammar of generic arguments *)
+
+let () =
+  let open Stdarg in
+  let open Constrarg in
+(*   Grammar.register0 wit_unit; *)
+(*   Grammar.register0 wit_bool; *)
+  Grammar.register0 wit_int (Prim.integer);
+  Grammar.register0 wit_string (Prim.string);
+  Grammar.register0 wit_pre_ident (Prim.preident);
+  Grammar.register0 wit_int_or_var (Tactic.int_or_var);
+  Grammar.register0 wit_intro_pattern (Tactic.simple_intropattern);
+  Grammar.register0 wit_ident (Prim.ident);
+  Grammar.register0 wit_var (Prim.var);
+  Grammar.register0 wit_ref (Prim.reference);
+  Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis);
+  Grammar.register0 wit_sort (Constr.sort);
+  Grammar.register0 wit_constr (Constr.constr);
+  Grammar.register0 wit_constr_may_eval (Tactic.constr_may_eval);
+  Grammar.register0 wit_uconstr (Tactic.uconstr);
+  Grammar.register0 wit_open_constr (Tactic.open_constr);
+  Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings);
+  Grammar.register0 wit_bindings (Tactic.bindings);
+(*   Grammar.register0 wit_hyp_location_flag; *)
+  Grammar.register0 wit_red_expr (Tactic.red_expr);
+  Grammar.register0 wit_tactic (Tactic.tactic);
+  Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl);
+  ()
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7e0c89fd1..64f6f720c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -160,10 +160,13 @@ val uconstr : gram_universe
 val utactic : gram_universe
 val uvernac : gram_universe
 
+val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
+val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
+
 val get_entry : gram_universe -> string -> typed_entry
 
-val create_generic_entry : string -> ('a, rlevel) abstract_argument_type ->
-  'a Gram.entry
+val create_generic_entry : gram_universe -> string ->
+  ('a, rlevel) abstract_argument_type -> 'a Gram.entry
 
 module Prim :
   sig
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 5dbc340ca..9a53e2e16 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -9,6 +9,10 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Cctac
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
 
 DECLARE PLUGIN "cc_plugin"
 
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 2d096a108..2afbaca2c 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -95,7 +95,7 @@ let proof_mode : vernac_expr Gram.entry =
   Gram.entry_create "vernac:proof_command"
 (* Auxiliary grammar entry. *)
 let proof_instr : raw_proof_instr Gram.entry =
-  Pcoq.create_generic_entry "proof_instr" (Genarg.rawwit wit_proof_instr)
+  Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr)
 
 let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
   pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index 18570a684..35a5a7616 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
 let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index aec958689..7bd07f625 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -11,6 +11,10 @@
 (* ML names *)
 
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
 open Pp
 open Names
 open Nameops
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 3e8be3699..587d10d1c 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -15,6 +15,10 @@ open Goptions
 open Tacticals
 open Tacinterp
 open Libnames
+open Constrarg
+open Stdarg
+open Pcoq.Prim
+open Pcoq.Tactic
 
 DECLARE PLUGIN "ground_plugin"
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 61ada5cc8..e93c395e3 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -16,8 +16,12 @@ open Constrexpr
 open Indfun_common
 open Indfun
 open Genarg
+open Constrarg
 open Tacticals
 open Misctypes
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "recdef_plugin"
 
@@ -90,7 +94,7 @@ let out_disjunctive = function
   | loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
   | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected."
 
-ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat
+ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
 |   [ "as"  simple_intropattern(ipat) ] -> [ Some ipat ]
 | []  ->[ None ]
 END
@@ -149,7 +153,7 @@ let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genar
   Genarg.create_arg "function_rec_definition_loc"
 
 let function_rec_definition_loc =
-  Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
+  Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
 
 GEXTEND Gram
   GLOBAL: function_rec_definition_loc ;
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index bfc9c727d..bca1c2feb 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -18,6 +18,10 @@
 
 open Errors
 open Misctypes
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Tactic
 
 DECLARE PLUGIN "micromega_plugin"
 
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 04c62eb48..b314e0d85 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -19,6 +19,8 @@ DECLARE PLUGIN "omega_plugin"
 
 open Names
 open Coq_omega
+open Constrarg
+open Pcoq.Prim
 
 let eval_tactic name =
   let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 7a3d7936a..a15b0eb05 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -13,6 +13,10 @@ open Misctypes
 open Tacexpr
 open Geninterp
 open Quote
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "quote_plugin"
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 6b2b2bbfa..61efa9f54 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -12,6 +12,8 @@ DECLARE PLUGIN "romega_plugin"
 
 open Names
 open Refl_omega
+open Constrarg
+open Pcoq.Prim
 
 let eval_tactic name =
   let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 856ec0db5..cd1d704dd 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -14,6 +14,11 @@ open Libnames
 open Printer
 open Newring_ast
 open Newring
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "newring_plugin"
 
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 7da6df717..6c02a7202 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -13,6 +13,12 @@ open Names
 open Locus
 open Misctypes
 open Genredexpr
+open Stdarg
+open Constrarg
+open Extraargs
+open Pcoq.Constr
+open Pcoq.Prim
+open Pcoq.Tactic
 
 open Proofview.Notations
 open Sigma.Notations
@@ -143,7 +149,7 @@ END
 
 TACTIC EXTEND symmetry
   [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
-| [ "symmetry" clause(cl) ] -> [ Tactics.intros_symmetry cl ]
+| [ "symmetry" clause_dft_concl(cl) ] -> [ Tactics.intros_symmetry cl ]
 END
 
 (** Split *)
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 98868e8f9..d33ec91f9 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -10,6 +10,10 @@
 
 open Pp
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
 open Names
 open Tacexpr
 open Taccoerce
@@ -51,6 +55,14 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 | [ ] -> [ true ]
 END
 
+let pr_int _ _ _ i = Pp.int i
+
+let _natural = Pcoq.Prim.natural
+
+ARGUMENT EXTEND natural TYPED AS int PRINTED BY pr_int
+| [ _natural(i) ] -> [ i ]
+END
+
 let pr_orient = pr_orient () () ()
 
 
@@ -118,6 +130,8 @@ let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
 
 let glob_glob = Tacintern.intern_constr
 
+let pr_lconstr _ prc _ c = prc c
+
 let subst_glob = Tacsubst.subst_glob_constr_and_expr
 
 ARGUMENT EXTEND glob
@@ -135,6 +149,14 @@ ARGUMENT EXTEND glob
   [ constr(c) ] -> [ c ]
 END
 
+let l_constr = Pcoq.Constr.lconstr
+
+ARGUMENT EXTEND lconstr
+    TYPED AS constr
+    PRINTED BY pr_lconstr
+  [ l_constr(c) ] -> [ c ]
+END
+
 ARGUMENT EXTEND lglob
     PRINTED BY pr_globc
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 7df845e4b..14aa69875 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -21,6 +21,8 @@ val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg
 val pr_occurrences : int list or_var -> Pp.std_ppcmds
 val occurrences_of : int list -> Locus.occurrences
 
+val wit_natural : int Genarg.uniform_genarg_type
+
 val wit_glob :
   (constr_expr,
   Tacexpr.glob_constr_and_expr,
@@ -31,6 +33,11 @@ val wit_lglob :
   Tacexpr.glob_constr_and_expr,
   Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
 
+val wit_lconstr :
+  (constr_expr,
+  Tacexpr.glob_constr_and_expr,
+  Constr.t) Genarg.genarg_type
+
 val glob : constr_expr Pcoq.Gram.entry
 val lglob : constr_expr Pcoq.Gram.entry
 
@@ -53,7 +60,6 @@ val pr_by_arg_tac :
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
   raw_tactic_expr option -> Pp.std_ppcmds
 
-
 (** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ae8b83b95..0cc796886 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -10,7 +10,12 @@
 
 open Pp
 open Genarg
+open Stdarg
+open Constrarg
 open Extraargs
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 open Mod_subst
 open Names
 open Tacexpr
@@ -49,6 +54,8 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
 
+let clause = Pcoq.Tactic.clause_dft_concl
+
 TACTIC EXTEND replace
    ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
 -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
@@ -147,23 +154,23 @@ TACTIC EXTEND einjection
 | [ "einjection" quantified_hypothesis(h) ] -> [ injClause None true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 TACTIC EXTEND injection_as_main
-| [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+| [ "injection" constr_with_bindings(c) "as" intropattern_list(ipat)] ->
     [ elimOnConstrWithHoles (injClause (Some ipat)) false c ]
 END
 TACTIC EXTEND injection_as
-| [ "injection" "as" simple_intropattern_list(ipat)] ->
+| [ "injection" "as" intropattern_list(ipat)] ->
     [ injClause (Some ipat) false None ]
-| [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+| [ "injection" quantified_hypothesis(h) "as" intropattern_list(ipat) ] ->
     [ injClause (Some ipat) false (Some (induction_arg_of_quantified_hyp h)) ]
 END
 TACTIC EXTEND einjection_as_main
-| [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
+| [ "einjection" constr_with_bindings(c) "as" intropattern_list(ipat)] ->
     [ elimOnConstrWithHoles (injClause (Some ipat)) true c ]
 END
 TACTIC EXTEND einjection_as
-| [ "einjection" "as" simple_intropattern_list(ipat)] ->
+| [ "einjection" "as" intropattern_list(ipat)] ->
     [ injClause (Some ipat) true None ]
-| [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
+| [ "einjection" quantified_hypothesis(h) "as" intropattern_list(ipat) ] ->
     [ injClause (Some ipat) true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
diff --git a/tactics/g_auto.ml4 b/tactics/g_auto.ml4
index f4fae763f..788443944 100644
--- a/tactics/g_auto.ml4
+++ b/tactics/g_auto.ml4
@@ -10,6 +10,11 @@
 
 open Pp
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 open Tacexpr
 
 DECLARE PLUGIN "g_auto"
@@ -128,7 +133,7 @@ TACTIC EXTEND dfs_eauto
 END
 
 TACTIC EXTEND autounfold
-| [ "autounfold" hintbases(db) clause(cl) ] -> [ Eauto.autounfold_tac db cl ]
+| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> [ Eauto.autounfold_tac db cl ]
 END
 
 TACTIC EXTEND autounfold_one
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4
index 766593543..9ef154541 100644
--- a/tactics/g_class.ml4
+++ b/tactics/g_class.ml4
@@ -10,6 +10,11 @@
 
 open Misctypes
 open Class_tactics
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
+open Stdarg
+open Constrarg
 
 DECLARE PLUGIN "g_class"
 
diff --git a/toplevel/g_obligations.ml4 b/tactics/g_obligations.ml4
index 32ccf21d2..e67d70121 100644
--- a/toplevel/g_obligations.ml4
+++ b/tactics/g_obligations.ml4
@@ -16,6 +16,12 @@
 open Libnames
 open Constrexpr
 open Constrexpr_ops
+open Stdarg
+open Constrarg
+open Extraargs
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 (* We define new entries for programs, with the use of this module
  * Subtac. These entries are named Subtac.<foo>
@@ -34,7 +40,7 @@ type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_a
 let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
   Genarg.create_arg "withtac"
 
-let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac)
+let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac)
 
 GEXTEND Gram
   GLOBAL: withtac;
@@ -57,11 +63,11 @@ open Obligations
 let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
 
 VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl
-| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] ->
+| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
     [ obligation (num, Some name, Some t) tac ]
 | [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
     [ obligation (num, Some name, None) tac ]
-| [ "Obligation" integer(num) ":" lconstr(t) withtac(tac) ] ->
+| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
     [ obligation (num, None, Some t) tac ]
 | [ "Obligation" integer(num) withtac(tac) ] ->
     [ obligation (num, None, None) tac ]
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 8b012aa88..c4ef1f297 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -20,6 +20,11 @@ open Extraargs
 open Tacmach
 open Tacticals
 open Rewrite
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
 
 DECLARE PLUGIN "g_rewrite"
 
@@ -186,7 +191,7 @@ type binders_argtype = local_binder list
 let wit_binders =
  (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
 
-let binders = Pcoq.create_generic_entry "binders" (Genarg.rawwit wit_binders)
+let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders)
 
 open Pcoq
 
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 73f11d0be..5c5946542 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,4 +1,5 @@
 Extraargs
+G_obligations
 Coretactics
 Autorewrite
 Extratactics