The code for universes was not correct in many borderline cases.

[helm.git] / helm / software / components / ng_kernel / check.ml

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index c3695726bd37c20ed042d116f8ee2135f5ac86bf..63863ffe1326c4bc50bb239871a0cb1ce2d76494 100644 (file)
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -139,7 +139,7 @@ let _ =
   let _ = 
     let rec aux = function
       | a::b::tl ->
-         NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b)
+         NCicEnvironment.add_le_constraint true (mk_type a) (mk_type b)
       | _ -> ()
     in
        aux lll