let le_constraints = ref [] (* strict,a,b *)
-let resolve_universe u =
- HExtlib.list_findopt
- (fun (_,a,b) _ ->
- prerr_endline (NUri.name_of_uri a);
- if NUri.name_of_uri a = u then Some a
- else if NUri.name_of_uri b = u then Some b
- else None)
- !le_constraints
-;;
-
let rec le_path_uri avoid strict a b =
(not strict && NUri.eq a b) ||
List.exists
val sup : NCic.universe -> NCic.universe option
val pp_constraints: unit -> string
-val resolve_universe: string -> NUri.uri option
-
val get_checked_def:
NReference.reference ->
NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int