From 53182a673b2f3673fe9e878f373a8bafe6f65f75 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 7 Jul 2005 15:31:30 +0000 Subject: [PATCH] apply_tac now catches TypeChecerFailure and raises Failure --- helm/ocaml/tactics/primitiveTactics.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index b185d693c..00b6dac7e 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -371,8 +371,11 @@ let apply_tac_verbose ~term status = try apply_tac_verbose ~term status (* TODO cacciare anche altre eccezioni? *) - with CicUnification.UnificationFailure _ as e -> - raise (Fail (Printexc.to_string e)) + with + | CicUnification.UnificationFailure _ as e -> + raise (Fail (Printexc.to_string e)) + | CicTypeChecker.TypeCheckerFailure _ as e -> + raise (Fail (Printexc.to_string e)) (* TODO per implementare i tatticali e' necessario che tutte le tattiche sollevino _solamente_ Fail *) @@ -381,8 +384,11 @@ let apply_tac ~term = try apply_tac ~term status (* TODO cacciare anche altre eccezioni? *) - with CicUnification.UnificationFailure _ as e -> - raise (Fail (Printexc.to_string e)) + with + | CicUnification.UnificationFailure _ as e -> + raise (Fail (Printexc.to_string e)) + | CicTypeChecker.TypeCheckerFailure _ as e -> + raise (Fail (Printexc.to_string e)) in mk_tactic (apply_tac ~term) -- 2.39.2