diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-01 22:14:20 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-01 22:14:20 +0000 |
| commit | 2e529d8c54382aecc2f825c58c517cf3fa0f8786 (patch) | |
| tree | 26a422297e9d41df409992ec3387f20e89154490 /proofs | |
| parent | 14f6e7940436909c6f3bc1cc9f01464a556c1a45 (diff) | |
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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 16 | ||||
| -rw-r--r-- | proofs/refiner.mli | 4 |
2 files changed, 13 insertions, 7 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 85f8a4f0e..8ca157345 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 af9da961b..6d5f26bae 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 |