From 469128f88cdcaba09daf57b595541b67b8077ded Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 9 Oct 2005 13:42:52 +0000 Subject: [PATCH] More informative exceptions raised. --- helm/ocaml/tactics/primitiveTactics.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 -- 2.39.2