From 442c8011ba8aca1a0f37226bfe3033a220bb71e3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Apr 2008 14:31:03 +0000 Subject: [PATCH] the explicit type in a LetIn must be typecheckd before convertibility is checked --- helm/software/components/cic_proof_checking/cicTypeChecker.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index eb9d376f2..ab43c3732 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -1647,6 +1647,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | C.LetIn (n,s,ty,t) -> (* only to check if s is well-typed *) let ty',ugraph1 = type_of_aux ~logger context s ugraph in + let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in let b,ugraph1 = R.are_convertible ~subst ~metasenv context ty ty' ugraph1 in -- 2.39.2