From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 7 Apr 2008 14:31:03 +0000 (+0000)
Subject: the explicit type in a LetIn must be typecheckd before convertibility is checked
X-Git-Tag: make_still_working~5429
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=442c8011ba8aca1a0f37226bfe3033a220bb71e3;p=helm.git

the explicit type in a LetIn must be typecheckd before convertibility is checked
---

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