From 26a79004e47bbdc97df61015ce7e944eef14ac71 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 8 Sep 2014 10:23:12 +0200
Subject: Parsing of Type@{max(i,j)}.

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

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index be343b9873..272a18c3e1 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -152,8 +152,13 @@ GEXTEND Gram
   sort:
     [ [ "Set"  -> GSet
       | "Prop" -> GProp
-      | "Type" -> GType None
-      | "Type"; "@{"; id = ident; "}" -> GType (Some (Id.to_string id))
+      | "Type" -> GType []
+      | "Type"; "@{"; u = universe; "}" -> GType (List.map Id.to_string u)
+      ] ]
+  ;
+  universe:
+    [ [ "max("; ids = LIST1 ident SEP ","; ")" -> ids
+      | id = ident -> [id]
       ] ]
   ;
   lconstr:
-- 
cgit v1.2.3