- Fix hashing of levels to get the "right" order in universe contexts etc...

- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.

1 files changed, 8 insertions, 2 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 499e7b0531..81645a580f 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -152,7 +152,9 @@ GEXTEND Gram
   sort:
     [ [ "Set"  -> GSet
       | "Prop" -> GProp
-      | "Type" -> GType None ] ]
+      | "Type" -> GType None
+      | "Type"; "{"; id = string; "}" -> GType (Some id)
+      ] ]
   ;
   lconstr:
     [ [ c = operconstr LEVEL "200" -> c ] ]
@@ -277,13 +279,17 @@ GEXTEND Gram
       | c=operconstr LEVEL "9" -> (c,None) ] ]
   ;
   atomic_constr:
-    [ [ g=global -> CRef (g,None)
+    [ [ g=global; i=instance -> CRef (g,i)
       | s=sort -> CSort (!@loc,s)
       | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n))
       | s=string -> CPrim (!@loc, String s)
       | "_" -> CHole (!@loc, None, None)
       | id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ]
   ;
+  instance:
+    [ [ "@{"; l = LIST1 sort SEP ","; "}" -> Some l
+      | -> None ] ]
+  ;
   fix_constr:
     [ [ fx1=single_fix -> mk_single_fix fx1
       | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with";