Simplification of grammar_prod_item type.

Actually the identifier was never used and just carried along.

9 files changed, 25 insertions, 33 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0894e0378d..cbebcdfcd4 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -520,8 +520,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")),
-	 Some (Names.Id.of_string "c"))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
 
 let _ =
   try
@@ -537,8 +536,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")),
-	 Some (Names.Id.of_string "c"))]
+        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
 
 (* Setting printer of unbound global reference *)
 open Names
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 6069f4b4b2..bf0c4fc215 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -95,7 +95,7 @@ let make_prod_item = function
   | ExtNonTerminal (EntryName (nt, g), id) ->
       let nt = Genarg.unquote nt in
       <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
-      $mlexpr_of_prod_entry_key g$ (Some $mlexpr_of_ident id$) >>
+      $mlexpr_of_prod_entry_key g$ >>
 
 let mlexpr_of_clause cl =
   mlexpr_of_list (fun (a,_,b) -> mlexpr_of_list make_prod_item a) cl
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 4bc3a9e609..3bb86fcb20 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -205,7 +205,7 @@ type proof_expr =
 
 type grammar_tactic_prod_item_expr =
   | TacTerm of string
-  | TacNonTerm of Loc.t * string * (Names.Id.t * string) option
+  | TacNonTerm of Loc.t * string * (Names.Id.t * string)
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index bd9bacbc60..29f8555c81 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -257,7 +257,7 @@ let add_ml_tactic_entry name prods =
   let mkact i loc l : raw_tactic_expr =
     let open Tacexpr in
     let entry = { mltac_name = name; mltac_index = i } in
-    let map (_, arg) = TacGeneric arg in
+    let map arg = TacGeneric arg in
     TacML (loc, entry, List.map map l)
   in
   let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
@@ -278,11 +278,10 @@ let add_tactic_entry kn tg =
   let mkact loc l =
     let filter = function
     | GramTerminal _ -> None
-    | GramNonTerminal (_, t, _, None) -> None
-    | GramNonTerminal (_, t, _, Some _) -> Some (Genarg.unquote t)
+    | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t)
     in
     let types = List.map_filter filter tg.tacgram_prods in
-    let map (id, arg) t =
+    let map arg t =
       (** HACK to handle especially the tactic(...) entry *)
       let wit = Genarg.rawwit Constrarg.wit_tactic in
       if Genarg.argument_type_eq t (Genarg.unquote wit) then
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 984027b815..e95b85bc26 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -18,9 +18,9 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      Loc.t * 'a raw_abstract_argument_type * ('s, 'a) entry_key * Id.t option -> 's grammar_prod_item
+      Loc.t * 'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's grammar_prod_item
 
-type 'a ty_arg = Id.t * ('a -> raw_generic_argument)
+type 'a ty_arg = ('a -> raw_generic_argument)
 
 type ('self, _, 'r) ty_rule =
 | TyStop : ('self, 'r, 'r) ty_rule
@@ -37,12 +37,9 @@ let rec ty_rule_of_gram = function
   let tok = Atoken (Lexer.terminal s) in
   let r = TyNext (rem, tok, None) in
   AnyTyRule r
-| GramNonTerminal (_, t, tok, idopt) :: rem ->
+| GramNonTerminal (_, t, tok) :: rem ->
   let AnyTyRule rem = ty_rule_of_gram rem in
-  let inj = match idopt with
-  | None -> None
-  | Some id -> Some (id, fun obj -> Genarg.in_gen t obj)
-  in
+  let inj = Some (fun obj -> Genarg.in_gen t obj) in
   let r = TyNext (rem, tok, inj) in
   AnyTyRule r
 
@@ -50,13 +47,13 @@ let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = func
 | TyStop -> Extend.Stop
 | TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok)
 
-type 'r gen_eval = Loc.t -> (Id.t * raw_generic_argument) list -> 'r
+type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r
 
 let rec ty_eval : type s a r. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function
 | TyStop -> fun f loc -> f loc []
 | TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f
-| TyNext (rem, tok, Some (id, inj)) -> fun f x ->
-  let f loc args = f loc ((id, inj x) :: args) in
+| TyNext (rem, tok, Some inj) -> fun f x ->
+  let f loc args = f loc (inj x :: args) in
   ty_eval rem f
 
 let make_rule f prod =
@@ -81,6 +78,6 @@ let get_extend_vernac_rule (s, i) =
 let extend_vernac_command_grammar s nt gl =
   let nt = Option.default Vernac_.command nt in
   vernac_exts := (s,gl) :: !vernac_exts;
-  let mkact loc l = VernacExtend (s,List.map snd l) in
+  let mkact loc l = VernacExtend (s, l) in
   let rules = [make_rule mkact gl] in
   grammar_extend nt None (None, [None, None, rules])
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index e3ae4e0118..8a494d70ba 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -16,7 +16,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type *
-      ('s, 'a) Pcoq.entry_key * Names.Id.t option -> 's grammar_prod_item
+      ('s, 'a) Pcoq.entry_key -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
   Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
@@ -27,5 +27,5 @@ val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_
 (** Utility function reused in Egramcoq : *)
 
 val make_rule :
-  (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'a) ->
+  (Loc.t -> Genarg.raw_generic_argument list -> 'a) ->
   'a grammar_prod_item list -> 'a Extend.production_rule
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2c9894dad2..f79aa8d3dd 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1165,7 +1165,7 @@ GEXTEND Gram
   production_item:
     [ [ s = ne_string -> TacTerm s
       | nt = IDENT;
-        po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ];
+        po = [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ];
                    ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ]
   ;
 END
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4957199903..daba18bad2 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -105,10 +105,9 @@ module Make
     else id
 
   let pr_production_item = function
-    | TacNonTerm (loc,nt,Some (p,sep)) ->
+    | TacNonTerm (loc, nt, (p, sep)) ->
       let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in
       str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")"
-    | TacNonTerm (loc,nt,None) -> str nt
     | TacTerm s -> qs s
 
   let pr_comment pr_c = function
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 821283e946..6ba5f4f875 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -47,10 +47,9 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
 let interp_prod_item lev = function
   | TacTerm s -> GramTerminal s
-  | TacNonTerm (loc, nt, po) ->
-      let sep = match po with Some (_,sep) -> sep | _ -> "" in
+  | TacNonTerm (loc, nt, (_, sep)) ->
       let EntryName (etyp, e) = interp_entry_name true (TgTactic lev) nt sep in
-      GramNonTerminal (loc, etyp, e, Option.map fst po)
+      GramNonTerminal (loc, etyp, e)
 
 let make_terminal_status = function
   | GramTerminal s -> Some s
@@ -58,7 +57,7 @@ let make_terminal_status = function
 
 let rec make_tags = function
   | GramTerminal s :: l -> make_tags l
-  | GramNonTerminal (loc, etyp, _, po) :: l -> Genarg.unquote etyp :: make_tags l
+  | GramNonTerminal (loc, etyp, _) :: l -> Genarg.unquote etyp :: make_tags l
   | [] -> []
 
 let make_fresh_key =
@@ -128,17 +127,17 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
        classify_function = classify_tactic_notation}
 
 let cons_production_parameter = function
-  | GramTerminal _ -> None
-  | GramNonTerminal (_, _, _, id) -> id
+| TacTerm _ -> None
+| TacNonTerm (_, _, (id, _)) -> Some id
 
 let add_tactic_notation (local,n,prods,e) =
+  let ids = List.map_filter cons_production_parameter prods in
   let prods = List.map (interp_prod_item n) prods in
   let tags = make_tags prods in
   let pprule = {
     Pptactic.pptac_args = tags;
     pptac_prods = (n, List.map make_terminal_status prods);
   } in
-  let ids = List.map_filter cons_production_parameter prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
   let parule = {
     tacgram_level = n;