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 895d157dfe9e26b3ad53ded633035a88b16fcd8b..1b159510063ce13dfddb3f7b60fc881c84dfcde7 100644 (file)
--- 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