exception BadDependency of string Lazy.t * exn;;
exception BadConstraint of string Lazy.t;;
+let get_obj = ref (fun _ -> assert false);;
+let set_get_obj f = get_obj := f;;
+
let type0 = []
let max l1 l2 =
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
Not_found ->
let saved_frozen_list = !frozen_list in
try
- let obj =
- try NCicLibrary.get_obj u
- with
- NCicLibrary.ObjectNotFound m -> raise (ObjectNotFound m)
- in
- frozen_list := (u,obj)::saved_frozen_list;
- !typecheck_obj obj;
- frozen_list := saved_frozen_list;
- let obj = `WellTyped obj in
- NUri.UriHash.add cache u obj;
- obj
+ let obj = !get_obj u in
+ frozen_list := (u,obj)::saved_frozen_list;
+ !typecheck_obj obj;
+ frozen_list := saved_frozen_list;
+ let obj = `WellTyped obj in
+ NUri.UriHash.add cache u obj;
+ obj
with
Sys.Break as e ->
frozen_list := saved_frozen_list;