More informative exceptions raised.

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index f38dd10b3108c13a991d6ad00b73b0868bbb0ca3..74a9f63f2548290bb22e136e58cf9ae2f9ee06f2 100644 (file)
--- 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