X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=2d52f0b8981a8352ef4de043df589cf342e8674e;hb=559a4d0ba0e52c99822ac636b1d635611ed9b5b8;hp=18c52b7cfa92a957729352e2a10ed4b2e31ddd5d;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index 18c52b7cf..2d52f0b89 100644
--- a/matita/components/content_pres/cicNotationParser.ml
+++ b/matita/components/content_pres/cicNotationParser.ml
@@ -582,9 +582,7 @@ EXTEND
     [ "Prop" -> `Prop
     | "Set" -> `Set
     | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n
-    | "Type" -> `Type (CicUniv.fresh ()) 
     | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
-    | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];
   explicit_subst: [