From 20c98eab851210702b39e1c66e005acfc351d8dd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 1 Dec 2017 10:11:41 +0100
Subject: Proper nametab handling of global universe names

They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
---
 parsing/g_constr.ml4 | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 7e5933cea2..0cf96d487b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -155,9 +155,15 @@ GEXTEND Gram
       | "Type" -> Sorts.InType
       ] ]
   ;
+  universe_expr:
+    [ [ id = global; "+"; n = natural -> Some (id,n)
+      | id = global -> Some (id,0)
+      | "_" -> None
+    ] ]
+  ;
   universe:
-    [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids
-      | id = name -> [id]
+    [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> ids
+      | u = universe_expr -> [u]
       ] ]
   ;
   lconstr:
@@ -307,8 +313,9 @@ GEXTEND Gram
   universe_level:
     [ [ "Set" -> GSet
       | "Prop" -> GProp
-      | "Type" -> GType None
-      | id = name -> GType (Some id)
+      | "Type" -> GType UUnknown
+      | "_" -> GType UAnonymous
+      | id = global -> GType (UNamed id)
       ] ]
   ;
   fix_constr:
-- 
cgit v1.2.3