more verbose case failure message

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 74542a22696ce39cac7d3d9e81f63acf67a6817c..9f5b280af307a74a7b1b2a4801897ec11ec11e04 100644 (file)
--- 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