From f25396b3a35ea5cd64b8b68670e66a14a78c418c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Mar 2016 17:04:07 +0100
Subject: Further reducing the dependencies of the EXTEND macros.

---
 grammar/argextend.ml4    | 15 +++++----------
 grammar/grammar.mllib    |  7 -------
 grammar/q_util.ml4       |  2 +-
 grammar/tacextend.ml4    | 23 ++++-------------------
 grammar/vernacextend.ml4 | 20 ++++++++++++--------
 parsing/tok.ml           | 20 +++++++++++---------
 6 files changed, 33 insertions(+), 54 deletions(-)

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index bebde706e4..801229bcb9 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -16,11 +16,6 @@ open Extend
 let loc = CompatLoc.ghost
 let default_loc = <:expr< Loc.ghost >>
 
-let qualified_name loc s =
-  let path = CString.split '.' s in
-  let (name, path) = CList.sep_last path in
-  qualified_name loc path name
-
 let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>
 
 let rec make_wit loc = function
@@ -56,7 +51,7 @@ 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
+| <:expr< $lid:s$ >> -> (s : string) = x
 | _ -> false
 
 let make_extend loc s cl wit = match cl with
@@ -85,7 +80,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let glob = match g with
     | None ->
       begin match rawtyp with
-      | Genarg.ExtraArgType s' when CString.equal s s' ->
+      | Genarg.ExtraArgType s' when s = s' ->
         <:expr< fun ist v -> (ist, v) >>
       | _ ->
         <:expr< fun ist v ->
@@ -100,7 +95,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let interp = match f with
     | None ->
       begin match globtyp with
-      | Genarg.ExtraArgType s' when CString.equal s s' ->
+      | Genarg.ExtraArgType s' when s = s' ->
         <:expr< fun ist v -> Ftactic.return v >>
       | _ ->
 	<:expr< fun ist x ->
@@ -120,7 +115,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let subst = match h with
     | None ->
       begin match globtyp with
-      | Genarg.ExtraArgType s' when CString.equal s s' ->
+      | Genarg.ExtraArgType s' when s = s' ->
         <:expr< fun s v -> v >>
       | _ ->
         <:expr< fun s x ->
@@ -132,7 +127,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let dyn = match typ with
   | `Uniform typ ->
     let is_new = match typ with
-    | Genarg.ExtraArgType s' when CString.equal s s' -> true
+    | Genarg.ExtraArgType s' when s = s' -> true
     | _ -> false
     in
     if is_new then <:expr< None >>
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 42fc738783..9b24c97974 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -1,15 +1,8 @@
 Coq_config
 
-Hashset
-Hashcons
-CMap
-Int
-Option
 Store
 Exninfo
 Loc
-CList
-CString
 
 Tok
 Compat
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index d91bfd7b8d..bde1e76517 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -57,7 +57,7 @@ let rec mlexpr_of_prod_entry_key f = function
   | Extend.Uentry e -> <:expr< Extend.Aentry $f e$ >>
   | Extend.Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
-    assert (CString.equal e "tactic");
+    assert (e = "tactic");
     if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
     else <:expr< Extend.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
 
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 1951b8b452..a34b880ae4 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -24,15 +24,6 @@ let rec make_patt = function
       <:patt< [ $lid:p$ :: $make_patt l$ ] >>
   | _::l -> make_patt l
 
-let rec mlexpr_of_argtype loc = function
-  | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
-  | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
-  | Genarg.PairArgType (t1,t2) ->
-      let t1 = mlexpr_of_argtype loc t1 in
-      let t2 = mlexpr_of_argtype loc t2 in
-      <:expr< Genarg.PairArgType $t1$ $t2$ >>
-  | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >>
-
 let rec make_let raw e = function
   | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
   | ExtNonTerminal (t, _, p) :: l ->
@@ -44,12 +35,6 @@ let rec make_let raw e = function
       <:expr< let $lid:p$ = $v$ in $e$ >>
   | _::l -> make_let raw e l
 
-let rec extract_signature = function
-  | [] -> []
-  | ExtNonTerminal (t, _, _) :: l -> t :: extract_signature l
-  | _::l -> extract_signature l
-
-
 let make_clause (pt,_,e) =
   (make_patt pt,
    vala None,
@@ -99,13 +84,13 @@ let declare_tactic loc s c cl = match cl with
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in
   let name = mlexpr_of_string name in
-  let tac =
+  let tac = match rem 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 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
       <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
   in
@@ -178,7 +163,7 @@ EXTEND
         let e = parse_user_entry e sep in
         ExtNonTerminal (type_of_user_symbol e, e, s)
       | s = STRING ->
-	let () = if CString.is_empty s then failwith "Empty terminal." in
+	let () = if s = "" then failwith "Empty terminal." in
         ExtTerminal s
     ] ]
   ;
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 453907689e..40e327c379 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -43,9 +43,11 @@ let make_clause { r_patt = pt; r_branch = e; } =
 
 (* To avoid warnings *)
 let mk_ignore c pt =
-  let names = CList.map_filter (function
-  | ExtNonTerminal (_, _, p) -> Some p
-  | _ -> None) pt in
+  let fold accu = function
+  | ExtNonTerminal (_, _, p) -> p :: accu
+  | _ -> accu
+  in
+  let names = List.fold_left fold [] pt in
   let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in
   let names = List.fold_left fold <:expr< () >> names in
   <:expr< do { let _ = $names$ in $c$ } >>
@@ -99,10 +101,12 @@ let make_fun_classifiers loc s c l =
   let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in
   mlexpr_of_list (fun x -> x) cl
 
-let mlexpr_of_clause =
-  mlexpr_of_list
-    (fun { r_head = a; r_patt = b; } -> mlexpr_of_list make_prod_item
-       (Option.List.cons (Option.map (fun a -> ExtTerminal a) a) b))
+let mlexpr_of_clause cl =
+  let mkexpr { r_head = a; r_patt = b; } = match a with
+  | None -> mlexpr_of_list make_prod_item b
+  | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+  in
+  mlexpr_of_list mkexpr cl
 
 let declare_command loc s c nt cl =
   let se = mlexpr_of_string s in
@@ -160,7 +164,7 @@ EXTEND
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]";
         d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let () = if CString.is_empty s then failwith "Command name is empty." in
+      let () = if 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/parsing/tok.ml b/parsing/tok.ml
index 6b90086155..df7e7c2a6b 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -8,6 +8,8 @@
 
 (** The type of token for the Coq lexer and parser *)
 
+let string_equal (s1 : string) s2 = s1 = s2
+
 type t =
   | KEYWORD of string
   | PATTERNIDENT of string
@@ -21,16 +23,16 @@ type t =
   | EOI
 
 let equal t1 t2 = match t1, t2 with
-| IDENT s1, KEYWORD s2 -> CString.equal s1 s2
-| KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2
-| PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2
-| IDENT s1, IDENT s2 -> CString.equal s1 s2
-| FIELD s1, FIELD s2 -> CString.equal s1 s2
-| INT s1, INT s2 -> CString.equal s1 s2
-| INDEX s1, INDEX s2 -> CString.equal s1 s2
-| STRING s1, STRING s2 -> CString.equal s1 s2
+| IDENT s1, KEYWORD s2 -> string_equal s1 s2
+| KEYWORD s1, KEYWORD s2 -> string_equal s1 s2
+| PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2
+| IDENT s1, IDENT s2 -> string_equal s1 s2
+| FIELD s1, FIELD s2 -> string_equal s1 s2
+| INT s1, INT s2 -> string_equal s1 s2
+| INDEX s1, INDEX s2 -> string_equal s1 s2
+| STRING s1, STRING s2 -> string_equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
-| BULLET s1, BULLET s2 -> CString.equal s1 s2
+| BULLET s1, BULLET s2 -> string_equal s1 s2
 | EOI, EOI -> true
 | _ -> false
 
-- 
cgit v1.2.3


From f329e1e63eb29958c4cc0d7bddfdb84a754351d2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Mar 2016 17:55:15 +0100
Subject: Do not keep the argument type in ExtNonTerminal.

---
 grammar/argextend.ml4    | 10 +++++-----
 grammar/q_util.ml4       |  2 +-
 grammar/q_util.mli       |  2 +-
 grammar/tacextend.ml4    | 16 +++++++++-------
 grammar/vernacextend.ml4 |  9 +++++----
 5 files changed, 21 insertions(+), 18 deletions(-)

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 801229bcb9..a38f57cdc9 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -32,14 +32,14 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
 let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< (fun loc -> $act$) >>
-    | ExtNonTerminal (_, _, p) :: tl -> <:expr< (fun $lid:p$ -> $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< Extend.Atoken (Lexer.terminal $mlexpr_of_string s$) >>
-  | ExtNonTerminal (_, g, _) ->
+  | ExtNonTerminal (g, _) ->
     let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in
     mlexpr_of_prod_entry_key base g
 
@@ -55,7 +55,7 @@ let is_ident x = function
 | _ -> false
 
 let make_extend loc s cl wit = match cl with
-| [[ExtNonTerminal (_, Uentry e, id)], act] when is_ident id act ->
+| [[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$ =
@@ -223,10 +223,10 @@ EXTEND
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | s = STRING -> ExtTerminal s
     ] ]
   ;
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index bde1e76517..56deb61f3d 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -13,7 +13,7 @@ open Compat
 
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * string
+| ExtNonTerminal of Extend.user_symbol * string
 
 let mlexpr_of_list f l =
   List.fold_right
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 5f292baf32..c84e9d1406 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -10,7 +10,7 @@ open Compat (* necessary for camlp4 *)
 
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * string
+| ExtNonTerminal of Extend.user_symbol * string
 
 val mlexpr_of_list :  ('a -> MLast.expr) -> 'a list -> MLast.expr
 
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index a34b880ae4..51c382b3b7 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -20,13 +20,14 @@ let plugin_name = <:expr< __coq_plugin_name >>
 
 let rec make_patt = function
   | [] -> <:patt< [] >>
-  | ExtNonTerminal (_, _, p) :: l ->
+  | ExtNonTerminal (_, p) :: l ->
       <:patt< [ $lid:p$ :: $make_patt l$ ] >>
   | _::l -> make_patt l
 
 let rec make_let raw e = function
   | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
-  | ExtNonTerminal (t, _, p) :: l ->
+  | ExtNonTerminal (g, p) :: l ->
+      let t = type_of_user_symbol g in
       let loc = MLast.loc_of_expr e in
       let e = make_let raw e l in
       let v =
@@ -46,7 +47,8 @@ let make_fun_clauses loc s l =
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
-  | ExtNonTerminal (nt, g, id) ->
+  | ExtNonTerminal (g, id) ->
+    let nt = type_of_user_symbol g in
     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 base g$ >>
@@ -66,11 +68,11 @@ let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
 (** Special treatment of constr entries *)
 let is_constr_gram = function
 | ExtTerminal _ -> false
-| ExtNonTerminal (_, Extend.Uentry "constr", _) -> true
+| ExtNonTerminal (Extend.Uentry "constr", _) -> true
 | _ -> false
 
 let make_var = function
-  | ExtNonTerminal (_, _, p) -> Some p
+  | ExtNonTerminal (_, p) -> Some p
   | _ -> assert false
 
 let declare_tactic loc s c cl = match cl with
@@ -158,10 +160,10 @@ EXTEND
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | s = STRING ->
 	let () = if s = "" then failwith "Empty terminal." in
         ExtTerminal s
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 40e327c379..aedaead71a 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -30,7 +30,8 @@ type rule = {
 
 let rec make_let e = function
   | [] -> e
-  | ExtNonTerminal (t, _, p) :: l ->
+  | ExtNonTerminal (g, p) :: l ->
+      let t = type_of_user_symbol g in
       let loc = MLast.loc_of_expr e in
       let e = make_let e l in
       <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
@@ -44,7 +45,7 @@ let make_clause { r_patt = pt; r_branch = e; } =
 (* To avoid warnings *)
 let mk_ignore c pt =
   let fold accu = function
-  | ExtNonTerminal (_, _, p) -> p :: accu
+  | ExtNonTerminal (_, p) -> p :: accu
   | _ -> accu
   in
   let names = List.fold_left fold [] pt in
@@ -179,10 +180,10 @@ EXTEND
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | s = STRING ->
         ExtTerminal s
     ] ]
-- 
cgit v1.2.3


From a559727d0a219db79d4230cccc2b4e73c8fc30c8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Mar 2016 18:20:51 +0100
Subject: EXTEND macros use their own internal representations.

---
 grammar/argextend.ml4 | 30 +++++++++++-------------------
 grammar/q_util.ml4    | 41 ++++++++++++++++++++++++++++-------------
 grammar/q_util.mli    | 24 ++++++++++++++++++++----
 grammar/tacextend.ml4 |  2 +-
 4 files changed, 60 insertions(+), 37 deletions(-)

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index a38f57cdc9..f9f3ee988e 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -8,10 +8,8 @@
 
 (*i camlp4deps: "tools/compat5b.cmo" i*)
 
-open Genarg
 open Q_util
 open Compat
-open Extend
 
 let loc = CompatLoc.ghost
 let default_loc = <:expr< Loc.ghost >>
@@ -25,6 +23,10 @@ let rec make_wit loc = function
       <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >>
   | ExtraArgType s -> mk_extraarg loc s
 
+let is_self s = function
+| ExtraArgType s' -> s = s'
+| _ -> false
+
 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$ >>
@@ -79,30 +81,26 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   in
   let glob = match g with
     | None ->
-      begin match rawtyp with
-      | Genarg.ExtraArgType s' when s = s' ->
+      if is_self s rawtyp then
         <:expr< fun ist v -> (ist, v) >>
-      | _ ->
+      else
         <:expr< fun ist v ->
           let ans = out_gen $make_globwit loc rawtyp$
           (Tacintern.intern_genarg ist
           (Genarg.in_gen $make_rawwit loc rawtyp$ v)) in
           (ist, ans) >>
-      end
     | Some f ->
       <:expr< fun ist v -> (ist, $lid:f$ ist v) >>
   in
   let interp = match f with
     | None ->
-      begin match globtyp with
-      | Genarg.ExtraArgType s' when s = s' ->
+      if is_self s globtyp then
         <:expr< fun ist v -> Ftactic.return v >>
-      | _ ->
+      else
 	<:expr< fun ist x ->
           Ftactic.bind
 	    (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x))
             (fun v -> Ftactic.return (Tacinterp.Value.cast $make_topwit loc globtyp$ v)) >>
-      end
     | Some f ->
       (** Compatibility layer, TODO: remove me *)
       <:expr<
@@ -114,23 +112,17 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
       >> in
   let subst = match h with
     | None ->
-      begin match globtyp with
-      | Genarg.ExtraArgType s' when s = s' ->
+      if is_self s globtyp then
         <:expr< fun s v -> v >>
-      | _ ->
+      else
         <:expr< fun s x ->
           out_gen $make_globwit loc globtyp$
           (Tacsubst.subst_genarg s
             (Genarg.in_gen $make_globwit loc globtyp$ x)) >>
-      end
     | Some f -> <:expr< $lid:f$>> in
   let dyn = match typ with
   | `Uniform typ ->
-    let is_new = match typ with
-    | Genarg.ExtraArgType s' when s = s' -> true
-    | _ -> false
-    in
-    if is_new then <:expr< None >>
+    if is_self s typ then <:expr< None >>
     else <:expr< Some (Genarg.val_tag $make_topwit loc typ$) >>
   | `Specialized _ -> <:expr< None >>
   in
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 56deb61f3d..6821887327 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -8,12 +8,27 @@
 
 (* This file defines standard combinators to build ml expressions *)
 
-open Extend
 open Compat
 
+type argument_type =
+| ListArgType of argument_type
+| OptArgType of argument_type
+| PairArgType of argument_type * argument_type
+| ExtraArgType of string
+
+type user_symbol =
+| Ulist1 : user_symbol -> user_symbol
+| Ulist1sep : user_symbol * string -> user_symbol
+| Ulist0 : user_symbol -> user_symbol
+| Ulist0sep : user_symbol * string -> user_symbol
+| Uopt : user_symbol -> user_symbol
+| Umodifiers : user_symbol -> user_symbol
+| Uentry : string -> user_symbol
+| Uentryl : string * int -> user_symbol
+
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of Extend.user_symbol * string
+| ExtNonTerminal of user_symbol * string
 
 let mlexpr_of_list f l =
   List.fold_right
@@ -48,14 +63,14 @@ let mlexpr_of_ident id =
   <:expr< Names.Id.of_string $str:id$ >>
 
 let rec mlexpr_of_prod_entry_key f = function
-  | Extend.Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
-  | Extend.Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
-  | Extend.Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Umodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Uentry e -> <:expr< Extend.Aentry $f e$ >>
-  | Extend.Uentryl (e, l) ->
+  | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >>
+  | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
+  | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
+  | Umodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key f s$ >>
+  | Uentry e -> <:expr< Extend.Aentry $f e$ >>
+  | Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
     assert (e = "tactic");
     if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
@@ -63,10 +78,10 @@ let rec mlexpr_of_prod_entry_key f = function
 
 let rec type_of_user_symbol = function
 | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s ->
-  Genarg.ListArgType (type_of_user_symbol s)
+  ListArgType (type_of_user_symbol s)
 | Uopt s ->
-  Genarg.OptArgType (type_of_user_symbol s)
-| Uentry e | Uentryl (e, _) -> Genarg.ExtraArgType e
+  OptArgType (type_of_user_symbol s)
+| Uentry e | Uentryl (e, _) -> ExtraArgType e
 
 let coincide s pat off =
   let len = String.length pat in
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index c84e9d1406..7d4cc0200a 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -8,9 +8,25 @@
 
 open Compat (* necessary for camlp4 *)
 
+type argument_type =
+| ListArgType of argument_type
+| OptArgType of argument_type
+| PairArgType of argument_type * argument_type
+| ExtraArgType of string
+
+type user_symbol =
+| Ulist1 : user_symbol -> user_symbol
+| Ulist1sep : user_symbol * string -> user_symbol
+| Ulist0 : user_symbol -> user_symbol
+| Ulist0sep : user_symbol * string -> user_symbol
+| Uopt : user_symbol -> user_symbol
+| Umodifiers : user_symbol -> user_symbol
+| Uentry : string -> user_symbol
+| Uentryl : string * int -> user_symbol
+
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of Extend.user_symbol * string
+| ExtNonTerminal of user_symbol * string
 
 val mlexpr_of_list :  ('a -> MLast.expr) -> 'a list -> MLast.expr
 
@@ -28,8 +44,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 : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr
+val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr
 
-val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type
+val type_of_user_symbol : user_symbol -> argument_type
 
-val parse_user_entry : string -> string -> Extend.user_symbol
+val parse_user_entry : string -> string -> user_symbol
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 51c382b3b7..bbd3d8a62f 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -68,7 +68,7 @@ let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
 (** Special treatment of constr entries *)
 let is_constr_gram = function
 | ExtTerminal _ -> false
-| ExtNonTerminal (Extend.Uentry "constr", _) -> true
+| ExtNonTerminal (Uentry "constr", _) -> true
 | _ -> false
 
 let make_var = function
-- 
cgit v1.2.3