From: Andrea Asperti <andrea.asperti@unibo.it>
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