diff options
author | 2013-11-04 18:08:48 +0000 | |
---|---|---|
committer | 2013-11-04 18:08:48 +0000 | |
commit | 84b30df7b5ef9479a89de322bceee5619405d195 (patch) | |
tree | d9a4a351e60041fb5a989379cc23e41ad0ca0142 /proofs | |
parent | 5f4a61935e048a8e4490f5610e551d8844a373c4 (diff) |
Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was solved.
This made "autorewrite using tac" fail.
Spotted in CoLoR and Demos.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17059 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/proofview.ml | 16 | ||||
-rw-r--r-- | proofs/proofview.mli | 13 |
2 files changed, 22 insertions, 7 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index bbeed4ad1..950ee8a3c 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -277,8 +277,12 @@ let tclEXACTLY_ONCE e t = (* Focuses a tactic at a range of subgoals, found by their indices. *) -(* arnaud: bug if 0 goals ! *) -let tclFOCUS i j t = +exception NoSuchGoals +let _ = Errors.register_handler begin function + | NoSuchGoals -> Errors.error "No such goals." + | _ -> raise Errors.Unhandled +end +let tclFOCUS_gen nosuchgoal i j t = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in @@ -290,10 +294,10 @@ let tclFOCUS i j t = Proof.get >>= fun next -> Proof.set (unfocus context next) >> Proof.ret result - with e when Errors.noncritical e -> - (* spiwack: a priori the only possible exceptions are that of focus, - of course I haven't made them algebraic yet. *) - tclZERO e + with IndexOutOfRange -> nosuchgoal + +let tclFOCUS i j t = tclFOCUS_gen (tclZERO NoSuchGoals) i j t +let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t (* Dispatch tacticals are used to apply a different tactic to each goal under diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 8bd7b8a28..b9251fffb 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -167,9 +167,20 @@ val tclONCE : 'a tactic -> 'a tactic val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic (* Focuses a tactic at a range of subgoals, found by their indices. - The other goals are restored to the focus when the tactic is done. *) + The other goals are restored to the focus when the tactic is done. + + If the specified range doesn't correspond to existing goals, fails + with [NoSuchGoals]. *) +exception NoSuchGoals val tclFOCUS : int -> int -> 'a tactic -> 'a tactic +(* Focuses a tactic at a range of subgoals, found by their indices. + The other goals are restored to the focus when the tactic is done. + + If the specified range doesn't correspond to existing goals, behaves + like [tclUNIT ()]. *) +val tclTRYFOCUS : int -> int -> unit tactic -> unit tactic + (* Dispatch tacticals are used to apply a different tactic to each goal under consideration. They come in two flavours: [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic]. |