From 78c13cd96f536f2e122957852062b323e83dda42 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 13 Jan 2006 11:04:44 +0000 Subject: [PATCH] More informative error message. --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index cd742d4cd..a44c63469 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -2059,7 +2059,10 @@ let typecheck_obj0 ~logger uri ugraph = let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in if not b then raise (TypeCheckerFailure - (lazy "the type of the body is not the one expected")) + (lazy + ("the type of the body is not the one expected:\n" ^ + CicPp.ppterm ty_te ^ "\nvs\n" ^ + CicPp.ppterm ty))) else ugraph | C.Constant (_,None,ty,_,_) -> -- 2.39.2