From dbada2989e334756971c7bf69578c93b2e45643e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 4 Jun 2014 17:18:58 +0200
Subject: - 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.

---
 parsing/g_constr.ml4 | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'parsing')

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