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

1 files changed, 10 insertions, 6 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bbeed4ad10..950ee8a3cd 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