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

[helm.git] / helm / software / components / content_pres / cicNotationParser.ml

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 8ddb78781a1f74214bb7ad4cdebc8de8241693fc..14032d4512994e54c2c72fd404848a1ebee7e72b 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -581,8 +581,9 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n 
+    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n
     | "Type" -> `Type (CicUniv.fresh ()) 
+    | "CProp"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NCProp n
     | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];