From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 5 Dec 2001 15:32:08 +0000 (+0000)
Subject: Very stupid bug fixed: in is_small, I created an environment in reverse order.
X-Git-Tag: mlminidom_0_2_2~20
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dec21bc41bdb9e400b3c34452e9edd8077eb9b24;p=helm.git

Very stupid bug fixed: in is_small, I created an environment in reverse order.
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 895d157df..1b1595100 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1225,7 +1225,7 @@ and is_small paramsno c =
     | _ -> true (*CSC: we trust the type-checker *)
  in
   let (sx,dx) = split_prods paramsno c in
-   is_small_aux sx dx
+   is_small_aux (List.rev sx) dx
 
 and type_of t =
  type_of_aux' [] t