From 5b94b621e536ab79462d2b553868bee281776b57 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 27 Jan 2012 14:25:42 +0000
Subject: [PATCH] Better error messages.
---
.../components/grafite_engine/nCicCoercDeclaration.ml | 11 +++++++----
1 file changed, 7 insertions(+), 4 deletions(-)
diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index 929d11235..1c6c63ebc 100644
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -140,10 +140,13 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
let src = cleanup_skel status () src in
status, src, cpos
with
- | NCicUnification.UnificationFailure _
- | NCicUnification.Uncertain _
- | MultiPassDisambiguator.DisambiguationError _ ->
- raise (GrafiteTypes.Command_error "bad source pattern"))
+ | NCicUnification.UnificationFailure msg
+ | NCicUnification.Uncertain msg ->
+ raise (GrafiteTypes.Command_error ("bad source pattern: " ^
+Lazy.force msg))
+ | MultiPassDisambiguator.DisambiguationError _ ->
+ raise (GrafiteTypes.Command_error ("bad source pattern:
+disambiguation error")))
| _ -> assert false
in
aux 0 [] ty
--
2.39.5