3 files changed, 7 insertions, 7 deletions
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 97a3e89a59..984957589f 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -17,7 +17,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item
+      Loc.t * 'a raw_abstract_argument_type option * ('s, 'a) symbol -> 's grammar_prod_item
 
 type 'a ty_arg = ('a -> raw_generic_argument)
 
@@ -38,7 +38,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 = Some (fun obj -> Genarg.in_gen t obj) in
+  let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in
   let r = TyNext (rem, tok, inj) in
   AnyTyRule r
 
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 1ad9472007..29baaf052b 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -15,7 +15,7 @@ open Vernacexpr
 
 type 's grammar_prod_item =
   | GramTerminal of string
-  | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type *
+  | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type option *
       ('s, 'a) Extend.symbol -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 0f2ed88fea..15f100c3b0 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -146,12 +146,12 @@ GEXTEND Gram
     [ [ "Set"  -> GSet
       | "Prop" -> GProp
       | "Type" -> GType []
-      | "Type"; "@{"; u = universe; "}" -> GType (List.map (fun (loc,x) -> (loc, Id.to_string x)) u)
+      | "Type"; "@{"; u = universe; "}" -> GType u
       ] ]
   ;
   universe:
-    [ [ IDENT "max"; "("; ids = LIST1 identref SEP ","; ")" -> ids
-      | id = identref -> [id]
+    [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids
+      | id = name -> [id]
       ] ]
   ;
   lconstr:
@@ -298,7 +298,7 @@ GEXTEND Gram
     [ [ "Set" -> GSet
       | "Prop" -> GProp
       | "Type" -> GType None
-      | id = identref -> GType (Some (fst id, Id.to_string (snd id)))
+      | id = name -> GType (Some id)
       ] ]
   ;
   fix_constr: