From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 7 Dec 2001 17:08:07 +0000 (+0000)
Subject: The typing rule for LetIn was simply wrong. Fixed.
X-Git-Tag: mlminidom_0_2_2~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bcedd27eba5358f1b76f2fb4bbbcb14b24efb4af;p=helm.git

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 5363c5e64..569e44674 100644
--- 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