Do not keep the argument type in ExtNonTerminal.

5 files changed, 21 insertions, 18 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 801229bcb..a38f57cdc 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 bde1e7651..56deb61f3 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 5f292baf3..c84e9d140 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 a34b880ae..51c382b3b 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 40e327c37..aedaead71 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
     ] ]