From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 17 May 2008 13:19:22 +0000 (+0000)
Subject: Bug fixed: only Type < Type1 was declared.
X-Git-Tag: make_still_working~5184
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=64588ee1a349ea931782c8388f0dbcb9e15279ef;p=helm.git

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 63863ffe1..6c750c559 100644
--- 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