X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.mli;fp=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.mli;h=5128831bea9ed279a6097203e99e253578294e6c;hb=f8d45b2e4fa7817d7ef8312b3bb8a7439bd7fb8c;hp=35b97aa596a136b0b7e3cb2d45ec61c4acd4ea34;hpb=8e0e2b06cfc3fb3116e1fce632d9897fdbac9895;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 35b97aa59..5128831be 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -53,9 +53,6 @@ val ppsort : Format.formatter -> NCic.sort -> unit
 val pp_constraints: unit -> string
 val get_universes: unit -> NCic.universe list
 
-(* The type of Prop, smaller than any other type *)
-val type0: NCic.universe
-
 (* use to type products *)
 val max: NCic.universe -> NCic.universe -> NCic.universe
 
@@ -65,6 +62,7 @@ exception BadConstraint of string Lazy.t;;
 val add_lt_constraint: NCic.universe -> NCic.universe -> unit
 val universe_eq: NCic.universe -> NCic.universe -> bool
 val universe_leq: NCic.universe -> NCic.universe -> bool
+val universe_lt: NCic.universe -> NCic.universe -> bool
 
 (* checks if s1 <= s2 *)
 val are_sorts_convertible: test_eq_only:bool -> NCic.sort -> NCic.sort -> bool
@@ -79,6 +77,8 @@ val typeof_sort: NCic.sort -> NCic.sort
 
 (* looks for a declared universe that is the least one above the input *)
 val sup : NCic.universe -> NCic.universe option
+val inf : strict:bool -> NCic.universe -> NCic.universe option
+val family_of : NCic.universe -> [ `CProp | `Type ]
 
 (* =========== /universes ============= *)