new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_as...

[helm.git] / helm / software / components / ng_kernel / nCicEnvironment.mli

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 35b97aa596a136b0b7e3cb2d45ec61c4acd4ea34..5128831bea9ed279a6097203e99e253578294e6c 100644 (file)
--- 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 ============= *)