diff options
| -rw-r--r-- | proofs/refiner.ml | 16 | ||||
| -rw-r--r-- | proofs/refiner.mli | 4 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 5 |
3 files changed, 15 insertions, 10 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 diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index e6172d3df..c6804329b 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -248,10 +248,9 @@ module SearchProblem = struct (* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) ((lgls,v'),pptac) :: aux tacl - with e when Logic.catchable_exception e -> - aux tacl + with e -> Refiner.catch_failerror e; aux tacl in aux l - + (* Ordering of states is lexicographic on depth (greatest first) then number of remaining goals. *) let compare s s' = |