From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 9 Oct 2005 13:42:52 +0000 (+0000)
Subject: More informative exceptions raised.
X-Git-Tag: V_0_7_2_3~229
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=469128f88cdcaba09daf57b595541b67b8077ded;p=helm.git

More informative exceptions raised.
---

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index f38dd10b3..74a9f63f2 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -325,8 +325,8 @@ let apply_tac_verbose_with_subst ~term status =
     apply_tac_verbose_with_subst ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with 
-  | CicUnification.UnificationFailure _ as e -> 
-      raise (Fail (Printexc.to_string e))
+  | CicUnification.UnificationFailure msg -> 
+      raise (Fail (CicUnification.explain_error msg))
   | CicTypeChecker.TypeCheckerFailure _ as e ->
       raise (Fail (Printexc.to_string e))
 
@@ -345,8 +345,8 @@ let apply_tac ~term =
     apply_tac ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with 
-  | CicUnification.UnificationFailure _ as e ->
-      raise (Fail (Printexc.to_string e))
+  | CicUnification.UnificationFailure msg ->
+      raise (Fail (CicUnification.explain_error msg))
   | CicTypeChecker.TypeCheckerFailure _ as e ->
       raise (Fail (Printexc.to_string e))
  in