- Better parsing and printing of named universes: Type{ident} and foo@{(ident|Prop|Set|Type|' ')*}

(user given names are still write only).
- Add test-suite file for named universes.

1 files changed, 9 insertions, 2 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 69ba73c673..86fa5518cc 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -153,7 +153,7 @@ GEXTEND Gram
     [ [ "Set"  -> GSet
       | "Prop" -> GProp
       | "Type" -> GType None
-      | "Type"; "{"; id = string; "}" -> GType (Some id)
+      | "Type"; "{"; id = ident; "}" -> GType (Some (Id.to_string id))
       ] ]
   ;
   lconstr:
@@ -287,9 +287,16 @@ GEXTEND Gram
       | id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ]
   ;
   instance:
-    [ [ "@{"; l = LIST1 sort SEP ","; "}" -> Some l
+    [ [ "@{"; l = LIST1 level; "}" -> Some l
       | -> None ] ]
   ;
+  level:
+    [ [ "Set" -> GSet
+      | "Prop" -> GProp
+      | "Type" -> GType None
+      | id = ident -> GType (Some (Id.to_string id))
+      ] ]
+  ;
   fix_constr:
     [ [ fx1=single_fix -> mk_single_fix fx1
       | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with";