X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=bae4a8f593628821b0f8d1181563aa7e496222b8;hb=6719c0e318b312b51b089fea3d69d1b7103245ea;hp=5aac1ef7da2422b9371febffda764fb250a9ca63;hpb=28f01bb2d0e5f1b3f180b0b478267d2beb06a5fe;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 5aac1ef7d..bae4a8f59 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -427,7 +427,7 @@ EXTEND
     [ "Prop" -> `Prop
     | "Set" -> `Set
     | "Type" -> `Type (CicUniv.fresh ()) 
-    | "CProp" -> `CProp
+    | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];
   explicit_subst: [