]> matita.cs.unibo.it Git - helm.git/commitdiff
the explicit type in a LetIn must be typecheckd before convertibility is checked
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 7 Apr 2008 14:31:03 +0000 (14:31 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 7 Apr 2008 14:31:03 +0000 (14:31 +0000)
helm/software/components/cic_proof_checking/cicTypeChecker.ml

index eb9d376f2aea3841eae4f0a96236bd5b690fceb9..ab43c3732ee6b1b572bfb66ed486ecd8439e7838 100644 (file)
@@ -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