The typing rule for LetIn was simply wrong. Fixed.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 5363c5e64f3294a7c06c43277826c33065207d8e..569e4467455f3e112b47297c5fe807b4d9472859 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1024,9 +1024,8 @@ and type_of_aux' env t =
          let _ = sort_of_prod (sort1,sort2) in
           C.Prod (n,s,type2)
    | C.LetIn (n,s,t) ->
-       let type1 = type_of_aux env s in
-       let type2 = type_of_aux (type1::env) t in
-        type2
+       let t' = CicSubstitution.subst s t in
+        type_of_aux env t'
    | C.Appl (he::tl) when List.length tl > 0 ->
       let hetype = type_of_aux env he
       and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in