Added new syntax Type[n] where n is a number.

[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 e3e54f112a5730608644d65f28b6135df444f250..cd02c9d36070a011c46911210917e84246b0beb3 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -563,6 +563,7 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
+    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n 
     | "Type" -> `Type (CicUniv.fresh ()) 
     | "CProp" -> `CProp (CicUniv.fresh ())
     ]