Pass unnamed arguments to ML macros.

This was imposing a bit of useless burden on the API for no good reason.

4 files changed, 8 insertions, 10 deletions

diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index c5dedc880e..89caff847f 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -19,7 +19,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      ('a raw_abstract_argument_type option * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item
+      ('a raw_abstract_argument_type * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item
 
 type 'a ty_arg = ('a -> raw_generic_argument)
 
@@ -40,7 +40,7 @@ let rec ty_rule_of_gram = function
   AnyTyRule r
 | GramNonTerminal (_, (t, tok)) :: rem ->
   let AnyTyRule rem = ty_rule_of_gram rem in
-  let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in
+  let inj = Some (fun obj -> Genarg.in_gen t obj) in
   let r = TyNext (rem, tok, inj) in
   AnyTyRule r
 
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index c4f4fcfaa4..a90ef97e7d 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -17,7 +17,7 @@ open Vernacexpr
 
 type 's grammar_prod_item =
   | GramTerminal of string
-  | GramNonTerminal : ('a Genarg.raw_abstract_argument_type option *
+  | GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
       ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 015d5fabef..80312d94fa 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2497,8 +2497,7 @@ type classifier = Genarg.raw_generic_argument list -> vernac_classification
 type (_, _) ty_sig =
 | TyNil : (atts:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
-| TyNonTerminal :
-  string option * ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
+| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
 
 type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
 
@@ -2511,7 +2510,7 @@ let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = functio
   | _ :: _ -> type_error ()
   end
 | TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args
-| TyNonTerminal (_, tu, ty) -> fun f args ->
+| TyNonTerminal (tu, ty) -> fun f args ->
   begin match args with
   | [] -> type_error ()
   | Genarg.GenArg (Rawwit tag, v) :: args ->
@@ -2528,7 +2527,7 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_comm
   | _ :: _ -> type_error ()
   end
 | TyTerminal (_, ty) -> fun f args -> untype_command ty f args
-| TyNonTerminal (_, tu, ty) -> fun f args ->
+| TyNonTerminal (tu, ty) -> fun f args ->
   begin match args with
   | [] -> type_error ()
   | Genarg.GenArg (Rawwit tag, v) :: args ->
@@ -2549,8 +2548,8 @@ let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s
 let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function
 | TyNil -> []
 | TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty
-| TyNonTerminal (id, tu, ty) ->
-  let t = Option.map (fun _ -> rawwit (Egramml.proj_symbol tu)) id in
+| TyNonTerminal (tu, ty) ->
+  let t = rawwit (Egramml.proj_symbol tu) in
   let symb = untype_user_symbol tu in
   Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
 
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index fb2a30bac7..34f6029e78 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -51,7 +51,6 @@ type (_, _) ty_sig =
 | TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal :
-  string option *
   ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
     ('a -> 'r, 'a -> 's) ty_sig