]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: only Type < Type1 was declared.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 17 May 2008 13:19:22 +0000 (13:19 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 17 May 2008 13:19:22 +0000 (13:19 +0000)
helm/software/components/ng_kernel/check.ml

index 63863ffe1326c4bc50bb239871a0cb1ce2d76494..6c750c55909f6b289627d5a33231807fe06ed915 100644 (file)
@@ -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