X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=ab43c3732ee6b1b572bfb66ed486ecd8439e7838;hb=442c8011ba8aca1a0f37226bfe3033a220bb71e3;hp=eb9d376f2aea3841eae4f0a96236bd5b690fceb9;hpb=080122687296a86b1a0c1e1ed67fb7a79bd84ec6;p=helm.git

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