From 342a8c82429c483e2ca872016a8e29cf8d3cfb56 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 31 May 2005 09:42:30 +0000 Subject: [PATCH] more verbose case failure message --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 74542a226..9f5b280af 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1680,8 +1680,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = else raise (TypeCheckerFailure (sprintf - ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri) i)) + ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") + (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)) | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> if U.eq uri uri' && i = i' then @@ -1691,8 +1691,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = else raise (TypeCheckerFailure (sprintf - "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}" - (CicPp.ppterm typ') (U.string_of_uri uri) i)) + ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") + (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)) | _ -> raise (TypeCheckerFailure -- 2.39.2