X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic.ml;h=c531d1c2bf9c7256c4886bde8bbd6780e68f23b0;hb=8b1a49bbee9eea86eb74c040defe701370ca5893;hp=e520422160ab7fc77a41069b3970b960c4b2ca6d;hpb=41068e795dcb5fd0e2f87d755d7f12b3cbb0f79b;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index e52042216..c531d1c2b 100644
--- a/helm/software/components/ng_kernel/nCic.ml
+++ b/helm/software/components/ng_kernel/nCic.ml
@@ -13,7 +13,9 @@
 
 (********************************* TERMS ************************************)
 
-type universe = (bool * NUri.uri) list 
+type univ_algebra = [ `Type | `Succ | `CProp ]
+
+type universe = (univ_algebra * NUri.uri) list 
   (* Max of non-empty list of named universes, or their successor (when true) 
    * The empty list represents type0 *)