From bcedd27eba5358f1b76f2fb4bbbcb14b24efb4af Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 7 Dec 2001 17:08:07 +0000 Subject: [PATCH] The typing rule for LetIn was simply wrong. Fixed. --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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 -- 2.39.2