]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationParser.ml
added universes
[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml
index bcfd6c9f62282e15163a5e988beb3a736702d41a..4622f67a6f1eff41881d7c3939a3dfe55fc9097d 100644 (file)
@@ -425,7 +425,7 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type" -> `Type
+    | "Type" -> `Type (CicUniv.fresh ()) 
     | "CProp" -> `CProp
     ]
   ];