From 2e529d8c54382aecc2f825c58c517cf3fa0f8786 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 1 May 2008 22:14:20 +0000
Subject: Move exception-handling code for catching tactics failure in a
 separate function in Refiner and use it in eauto to capture the same
 semantics as auto (which uses tclTRY) when trying tactics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10879 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/refiner.ml  | 16 +++++++++-------
 proofs/refiner.mli |  4 ++++
 2 files changed, 13 insertions(+), 7 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 85f8a4f0e0..8ca1573457 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -492,19 +492,21 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
       (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
 
-
+let catch_failerror = function
+  | e when catchable_exception e -> check_for_interrupt ()
+  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) ->
+      check_for_interrupt ()
+  | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
+  | Stdpp.Exc_located (s,FailError (lvl,s')) ->
+      raise (Stdpp.Exc_located (s,FailError (lvl - 1, s')))
+  | _ -> ()
 
 (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
 let tclORELSE0 t1 t2 g =
   try 
     t1 g
   with (* Breakpoint *)
-  | e when catchable_exception e -> check_for_interrupt (); t2 g
-  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) ->
-      check_for_interrupt (); t2 g
-  | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
-  | Stdpp.Exc_located (s,FailError (lvl,s')) ->
-      raise (Stdpp.Exc_located (s,FailError (lvl - 1, s')))
+    | e -> catch_failerror e; t2 g
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, 
    then applies t2 *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index af9da961ba..6d5f26bae0 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -133,6 +133,10 @@ val tclTHENFIRSTn   : tactic -> tactic array -> tactic
 (* A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.std_ppcmds
 
+(* Takes an exception and either raise it at the next
+   level or do nothing. *)
+val catch_failerror  : exn -> unit
+
 val tclORELSE        : tactic -> tactic -> tactic
 val tclREPEAT        : tactic -> tactic
 val tclREPEAT_MAIN   : tactic -> tactic
-- 
cgit v1.2.3