Allowing Set to be part of universe expressions.

Conversely, Type existential variables now (explicitly) cover the Set
case.

Similarly for Prop and SProp.

1 files changed, 25 insertions, 17 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index dd68b411a0..79cfe33b12 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -133,7 +133,8 @@ let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family
+  GLOBAL: binder_constr lconstr constr operconstr
+  universe_level universe_name sort sort_family
   global constr_pattern lconstr_pattern Constr.ident
   closed_binder open_binders binder binders binders_fixannot
   record_declaration typeclass_constraint pattern appl_arg;
@@ -153,11 +154,12 @@ GRAMMAR EXTEND Gram
     [ [ c = lconstr -> { c } ] ]
   ;
   sort:
-    [ [ "Set"  -> { GSet }
-      | "Prop" -> { GProp }
-      | "SProp" -> { GSProp }
-      | "Type" -> { GType UUnknown }
-      | "Type"; "@{"; u = universe; "}" -> { GType u }
+    [ [ "Set"  -> { UNamed [GSet,0] }
+      | "Prop" -> { UNamed [GProp,0] }
+      | "SProp" -> { UNamed [GSProp,0] }
+      | "Type" -> { UAnonymous {rigid=true} }
+      | "Type"; "@{"; "_"; "}" -> { UAnonymous {rigid=false} }
+      | "Type"; "@{"; u = universe; "}" -> { UNamed u }
       ] ]
   ;
   sort_family:
@@ -167,15 +169,21 @@ GRAMMAR EXTEND Gram
       | "Type" -> { Sorts.InType }
       ] ]
   ;
+  universe_increment:
+    [ [ "+"; n = natural -> { n }
+      | -> { 0 } ] ]
+  ;
+  universe_name:
+    [ [ id = global -> { GType id }
+      | "Set"  -> { GSet }
+      | "Prop" -> { GProp } ] ]
+  ;
   universe_expr:
-    [ [ id = global; "+"; n = natural -> { (id,n) }
-      | id = global -> { (id,0) }
-      ] ]
+    [ [ id = universe_name; n = universe_increment -> { (id,n) } ] ]
   ;
   universe:
-    [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { UNamed ids }
-      | u = universe_expr -> { UNamed [u] }
-      | "_" -> { UAnonymous }
+    [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids }
+      | u = universe_expr -> { [u] }
       ] ]
   ;
   lconstr:
@@ -328,12 +336,12 @@ GRAMMAR EXTEND Gram
       | -> { None } ] ]
   ;
   universe_level:
-    [ [ "Set" -> { GSet }
+    [ [ "Set" -> { UNamed GSet }
       (* no parsing SProp as a level *)
-      | "Prop" -> { GProp }
-      | "Type" -> { GType UUnknown }
-      | "_" -> { GType UAnonymous }
-      | id = global -> { GType (UNamed id) }
+      | "Prop" -> { UNamed GProp }
+      | "Type" -> { UAnonymous {rigid=true} }
+      | "_" -> { UAnonymous {rigid=false} }
+      | id = global -> { UNamed (GType id) }
       ] ]
   ;
   fix_constr: