As required by M. Maietti,

[helm.git] / matita / components / ng_kernel / nCicEnvironment.ml

diff --git a/matita/components/ng_kernel/nCicEnvironment.ml b/matita/components/ng_kernel/nCicEnvironment.ml
index 74e28ff9c7925c81bcb0ed0cdf7e5f01601e5209..991a88f6406a120b9066d9c28e062ce7ff1aa13b 100644 (file)
--- a/matita/components/ng_kernel/nCicEnvironment.ml
+++ b/matita/components/ng_kernel/nCicEnvironment.ml
@@ -155,11 +155,11 @@ let typeof_sort = function
   | 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 ()))));