diff options
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 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 |