X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=fa229d6f6752b5e82948af0d89f00041891c7193;hb=17a2d79ff87d6b1942772b516e4d633347419c2e;hp=ddfe2ca52361506466db29377d5a3be13bd705ea;hpb=b5f64556ec797a92c2c79d9d1c6aefa4dcf880b1;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index ddfe2ca52..fa229d6f6 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -20,18 +20,16 @@ let type0 = [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
 
 let le_constraints = ref [] (* strict,a,b *)
 
-let rec le_path_uri strict a b = 
- if strict then
-  List.exists (fun (strict,x,y) -> NUri.eq y b &&
-   if strict then le_path_uri false a x else le_path_uri strict a x)
-    !le_constraints
- else
-  NUri.eq a b ||
-   List.exists (fun (_,x,y) -> NUri.eq y b && le_path_uri false a x)
-     !le_constraints
+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
 ;;
 
-let leq_path a b = le_path_uri (fst a) (snd a) b;;
+let leq_path a b = le_path_uri [b] (fst a) (snd a) b;;
 
 let universe_leq a b = 
   match a, b with
@@ -45,9 +43,10 @@ let universe_eq a b = universe_leq b a || universe_leq a b
 let add_le_constraint strict a b = 
   match a,b with
   | [false,a2],[false,b2] -> 
-      if le_path_uri (not strict) b2 a2 then
-       (raise (BadConstraint (lazy "universe inconsistency")));
-      le_constraints := (strict,a2,b2) :: !le_constraints  
+      if not (le_path_uri [] strict a2 b2) then (
+        if le_path_uri [] (not strict) b2 a2 then
+         (raise (BadConstraint (lazy "universe inconsistency")));
+        le_constraints := (strict,a2,b2) :: !le_constraints)
   | _ -> raise (BadConstraint
           (lazy "trying to add a constraint on an inferred universe"))
 ;;