- cic almost not used

[helm.git] / matita / components / content / notationPt.ml

diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml
index 731a2ba7436f70b6c21f7b05ab0e0274118f9071..90990300abfc6b985bb5266b2ff5800987e53110 100644 (file)
--- a/matita/components/content/notationPt.ml
+++ b/matita/components/content/notationPt.ml
@@ -29,8 +29,7 @@
 
 type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
 type induction_kind = [ `Inductive | `CoInductive ]
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of
-CicUniv.universe | `NType of string |`NCProp of string]
+type sort_kind = [ `Prop | `Set | `NType of string |`NCProp of string]
 type fold_kind = [ `Left | `Right ]
 
 type location = Stdpp.location