in the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 742e538febd09a0f50b3780a319ac3d67a08c81d..396567a2e708f8b08bdc2972774c606738b5191c 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -664,7 +664,7 @@ EXTEND
           in
           L.Number_alias (instance, dsc)
       ]
-    ];
+     ];
     argument: [
       [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
         id = IDENT ->
@@ -785,6 +785,27 @@ EXTEND
             ind_types
         in
         G.NObj (loc, N.Inductive (params, ind_types))
+    | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; 
+        strict = [ SYMBOL <:unicode<lt>> -> true 
+                 | SYMBOL <:unicode<leq>> -> false ]; 
+        u2 = tactic_term ->
+        let u1 =
+          match u1 with
+          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
+              NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
+          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
+              NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
+          | _ -> raise (Failure "only a sort can be constrained")
+        in
+        let u2 =
+          match u2 with
+          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
+              NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
+          | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
+              NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
+          | _ -> raise (Failure "only a sort can be constrained")
+        in
+         G.NUnivConstraint (loc, strict,u1,u2)
     | IDENT "coercion" ; 
       t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
       arity = OPT int ; saturations = OPT int;