From de6e6c56b88c880e66523b0e166f744cf8c38e22 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 26 Apr 2002 10:31:06 +0000 Subject: [PATCH] Bug fixed in type_of_aux (Cast case). --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) -> -- 2.39.2