From 5b94b621e536ab79462d2b553868bee281776b57 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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.2