From: Andrea Asperti Date: Tue, 31 May 2005 09:42:30 +0000 (+0000) Subject: more verbose case failure message X-Git-Tag: PRE_INDEX_1~94 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=342a8c82429c483e2ca872016a8e29cf8d3cfb56;p=helm.git more verbose case failure message --- 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