From e9b745af47ba3386724b874e3fd74b6dad33b015 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 6 Apr 2017 22:48:32 +0200
Subject: Allow flexible anonymous universes in instances and sorts.

The addition to the test suite showcases the usage.
---
 parsing/g_constr.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'parsing')

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:
-- 
cgit v1.2.3


From cd3971e53b76cb62e14822eb3e275d3968a4f215 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 May 2017 22:30:09 +0200
Subject: Adding support for using grammar entries returning no value in
 EXTEND.

---
 parsing/egramml.ml  | 4 ++--
 parsing/egramml.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'parsing')

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 :
-- 
cgit v1.2.3