val get_relevance: #NCic.status -> NReference.reference -> bool list
+val get_checked_decl:
+ #NCic.status -> NReference.reference ->
+ NCic.relevance * string * NCic.term * NCic.c_attr * int
+
val get_checked_def:
#NCic.status -> NReference.reference ->
NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int
(* raise BadConstraints if the second arg. is an inferred universe or
* if the added constraint gives circularity *)
exception BadConstraint of string Lazy.t;;
-val add_lt_constraint: NCic.universe -> NCic.universe -> unit
+val add_lt_constraint: acyclic:bool -> 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