Towards unifying parsing/printing for universe instances and Type's argument.

We consistently use:
- UUnknown: to mean a rigid anonymous universe
  (written Type in instances and Type as a sort)
  [was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
  (written _ in instances and Type@{_} as a sort)
  [was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
  (written id or qualid in instances and Type@{id} or Type@{qualid} or more
   generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)

There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.

There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.

1 files changed, 7 insertions, 7 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index bd88570224..dd68b411a0 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -156,7 +156,7 @@ GRAMMAR EXTEND Gram
     [ [ "Set"  -> { GSet }
       | "Prop" -> { GProp }
       | "SProp" -> { GSProp }
-      | "Type" -> { GType [] }
+      | "Type" -> { GType UUnknown }
       | "Type"; "@{"; u = universe; "}" -> { GType u }
       ] ]
   ;
@@ -168,14 +168,14 @@ GRAMMAR EXTEND Gram
       ] ]
   ;
   universe_expr:
-    [ [ id = global; "+"; n = natural -> { Some (id,n) }
-      | id = global -> { Some (id,0) }
-      | "_" -> { None }
-    ] ]
+    [ [ id = global; "+"; n = natural -> { (id,n) }
+      | id = global -> { (id,0) }
+      ] ]
   ;
   universe:
-    [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids }
-      | u = universe_expr -> { [u] }
+    [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { UNamed ids }
+      | u = universe_expr -> { UNamed [u] }
+      | "_" -> { UAnonymous }
       ] ]
   ;
   lconstr: