Bug fixed: only Type < Type1 was declared.

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 63863ffe1326c4bc50bb239871a0cb1ce2d76494..6c750c55909f6b289627d5a33231807fe06ed915 100644 (file)
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -138,8 +138,9 @@ let _ =
   prerr_endline "caching objects";
   let _ = 
     let rec aux = function
-      | a::b::tl ->
-         NCicEnvironment.add_le_constraint true (mk_type a) (mk_type b)
+      | a::(b::_ as tl) ->
+         NCicEnvironment.add_le_constraint true (mk_type a) (mk_type b);
+         aux tl
       | _ -> ()
     in
        aux lll