huge commit regarding universes:

[helm.git] / helm / software / components / ng_kernel / nCic.ml

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index e520422160ab7fc77a41069b3970b960c4b2ca6d..c531d1c2bf9c7256c4886bde8bbd6780e68f23b0 100644 (file)
--- 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 *)