X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FnCicCoercDeclaration.ml;h=1c6c63ebc2feac4dd6e308d2b65778ad96503718;hb=fc59fdd74aefc06a7d11bab7ebaafda478c18f7e;hp=929d1123560a92103b8b8ddc34a9f88ae5830a2f;hpb=8aa44cb352041dd314011996b4b1a1ff8990a000;p=helm.git

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