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