From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 7 Jul 2005 15:31:30 +0000 (+0000)
Subject: apply_tac now catches TypeChecerFailure and raises Failure
X-Git-Tag: V_0_7_1~11
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=53182a673b2f3673fe9e878f373a8bafe6f65f75;p=helm.git

apply_tac now catches TypeChecerFailure and raises Failure
---

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)