From: Claudio Sacerdoti Coen 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/?a=commitdiff_plain;h=de6e6c56b88c880e66523b0e166f744cf8c38e22;p=helm.git 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) ->