X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=991a88f6406a120b9066d9c28e062ce7ff1aa13b;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=74e28ff9c7925c81bcb0ed0cdf7e5f01601e5209;hpb=f75b0191e4f4538ab5bfc47157438ac45bd26f16;p=helm.git

diff --git a/matita/components/ng_kernel/nCicEnvironment.ml b/matita/components/ng_kernel/nCicEnvironment.ml
index 74e28ff9c..991a88f64 100644
--- 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 ()))));