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 4ff7d93921f8ed2b284a02961adac4d589f4c741..884eb1944943653fa25e8e9c2ec27298c1a8fc90 100644 (file)
--- 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) ->