| C.Prop -> (C.Type [])
;;
-let add_lt_constraint a b =
+let add_lt_constraint ~acyclic a b =
match a,b with
| [`Type,a2],[`Type,b2] ->
if not (lt_path_uri [] a2 b2) then (
- if lt_path_uri [] b2 a2 || NUri.eq a2 b2 then
+ if acyclic && (lt_path_uri [] b2 a2 || NUri.eq a2 b2) then
(raise(BadConstraint(lazy("universe inconsistency adding "^
pp_constraint a2 b2
^ " to:\n" ^ pp_constraints ()))));
| e ->
frozen_list := saved_frozen_list;
let exn = `Exn e in
- NUri.UriHash.add cache u exn;
history := (`Obj (u,obj))::!history;
if saved_frozen_list = [] then
exn
else
- raise (Propagate (u,e))
+ begin
+ NUri.UriHash.add cache u exn;
+ raise (Propagate (u,e))
+ end
;;
let get_checked_obj status u =