-exception BadDependency of string Lazy.t;;
-
-let type0 = [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
-
-let u_eq (a1,a2) (b1,b2) = a1=b1 && NUri.eq a2 b2
-
-let u_lt a b =
- match a,b with
- | (false,a2), (true,b2) -> NUri.eq a2 b2
- | _ -> false
+exception BadDependency of string Lazy.t * exn;;
+exception BadConstraint of string Lazy.t;;
+
+let type0 = []
+
+let max l1 l2 =
+ HExtlib.list_uniq ~eq:(fun (b1,u1) (b2,u2) -> b1=b2 && NUri.eq u1 u2)
+ (List.sort (fun (b1,u1) (b2,u2) ->
+ let res = compare b1 b2 in if res = 0 then NUri.compare u1 u2 else res)
+ (l1 @ l2))
+
+let le_constraints = ref [] (* strict,a,b *)
+
+let rec le_path_uri avoid strict a b =
+ (not strict && NUri.eq a b) ||
+ List.exists
+ (fun (strict',x,y) ->
+ NUri.eq y b && not (List.exists (NUri.eq x) avoid) &&
+ le_path_uri (x::avoid) (strict && not strict') a x
+ ) !le_constraints