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

3 files changed, 23 insertions, 8 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
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 8bd7b8a283..b9251fffbb 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].
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f815830ca2..639c4c97bc 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -495,7 +495,7 @@ module New = struct
     tclREPEAT0 (tclPROGRESS t)
   let rec tclREPEAT_MAIN0 t =
     tclIFCATCH t
-      (fun () -> tclFOCUS 1 1 (tclREPEAT_MAIN0 t))
+      (fun () -> tclTRYFOCUS 1 1 (tclREPEAT_MAIN0 t))
       (fun e -> catch_failerror e <*> tclUNIT ())
   let tclREPEAT_MAIN t =
     tclREPEAT_MAIN0 (tclPROGRESS t)