From b720cd3cbefa46da784b68a8e016a853f577800c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Aug 2014 12:53:39 +0200
Subject: No plural for only one non existing focused goal.

---
 proofs/proofview.ml  | 6 +++---
 proofs/proofview.mli | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 661b32601c..0acfda3d80 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -309,9 +309,9 @@ let tclEXACTLY_ONCE e t =
 
 
 (* Focuses a tactic at a range of subgoals, found by their indices. *)
-exception NoSuchGoals
+exception NoSuchGoals of int
 let _ = Errors.register_handler begin function
-  | NoSuchGoals -> Errors.error "No such goals."
+  | NoSuchGoals n -> Errors.error ("No such " ^ String.plural n "goal" ^".")
   | _ -> raise Errors.Unhandled
 end
 let tclFOCUS_gen nosuchgoal i j t =
@@ -327,7 +327,7 @@ let tclFOCUS_gen nosuchgoal i j t =
     Proof.ret result
   with IndexOutOfRange -> nosuchgoal
 
-let tclFOCUS i j t = tclFOCUS_gen (tclZERO NoSuchGoals) i j t
+let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t
 let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
 
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 6816908109..b1ff30ee9b 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -194,7 +194,7 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
 
    If the specified range doesn't correspond to existing goals, fails
    with [NoSuchGoals]. *)
-exception NoSuchGoals
+exception NoSuchGoals of int
 val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
 
 (* Focuses a tactic at a range of subgoals, found by their indices.
-- 
cgit v1.2.3