apply_tac now catches TypeChecerFailure and raises Failure

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