From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 26 Apr 2002 10:31:06 +0000 (+0000)
Subject: Bug fixed in type_of_aux (Cast case).
X-Git-Tag: V_0_3_0_debian_8~127
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=de6e6c56b88c880e66523b0e166f744cf8c38e22

Bug fixed in type_of_aux (Cast case).
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 4ff7d9392..884eb1944 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1047,7 +1047,7 @@ and type_of_aux' metasenv context t =
     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | C.Implicit -> raise (Impossible 21)
     | C.Cast (te,ty) ->
-       let _ = type_of ty in
+       let _ = type_of_aux context ty in
         if R.are_convertible (type_of_aux context te) ty then ty
         else raise (NotWellTyped "Cast")
     | C.Prod (_,s,t) ->