Fix proof bullet error helper (nosuchgoal)

The [int] is incorrect for list focusing, we could work a bit harder
to fix that. It's only used for pluralisation in the error message "no
such goal(s)" so we could also ignore the issue.

4 files changed, 22 insertions, 36 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 86dcb8ab3b..f278c83912 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -352,11 +352,12 @@ let _ = CErrors.register_handler begin function
   | _ -> raise CErrors.Unhandled
 end
 
-(** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where
+(** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where
     only the goals numbered [i] to [j] are focused (the rest of the goals
     is restored at the end of the tactic). If the range [i]-[j] is not
     valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *)
-let tclFOCUS_gen nosuchgoal i j t =
+let tclFOCUS ?nosuchgoal i j t =
+  let nosuchgoal = Option.default (tclZERO (NoSuchGoals (j+1-i))) nosuchgoal in
   let open Proof in
   Pv.get >>= fun initial ->
   try
@@ -367,10 +368,9 @@ let tclFOCUS_gen nosuchgoal i j t =
     return result
   with CList.IndexOutOfRange -> nosuchgoal
 
-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
+let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
 
-let tclFOCUSLIST l t =
+let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t =
   let open Proof in
   Comb.get >>= fun comb ->
     let n = CList.length comb in
@@ -384,7 +384,7 @@ let tclFOCUSLIST l t =
     in
     let l = CList.map_filter sanitize l in
     match l with
-      | [] -> tclZERO (NoSuchGoals 0)
+      | [] -> nosuchgoal
       | (mi, _) :: _ ->
           (* Get the left-most goal to focus. This goal won't move, and we
              will then place all the other goals to focus to the right. *)
@@ -401,7 +401,7 @@ let tclFOCUSLIST l t =
 
 
 (** Like {!tclFOCUS} but selects a single goal by name. *)
-let tclFOCUSID id t =
+let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
   let open Proof in
   Pv.get >>= fun initial ->
   try
@@ -421,7 +421,7 @@ let tclFOCUSID id t =
         t >>= fun result ->
       Comb.set initial.comb  >>
         return result
-  with Not_found -> tclZERO (NoSuchGoals 1)
+  with Not_found -> nosuchgoal
 
 (** {7 Dispatching on goals} *)
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 8685430c62..9455dae643 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -244,14 +244,12 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
 (** [tclFOCUS i j t] applies [t] after focusing on the goals number
     [i] to [j] (see {!focus}). The rest of the goals is restored after
     the tactic action. If the specified range doesn't correspond to
-    existing goals, fails with [NoSuchGoals] (a user error). this
-    exception is caught at toplevel with a default message + a hook
-    message that can be customized by [set_nosuchgoals_hook] below.
-    This hook is used to add a suggestion about bullets when
-    applicable. *)
+    existing goals, fails with the [nosuchgoal] argument, by default
+    raising [NoSuchGoals] (a user error). This exception is caught at
+    toplevel with a default message. *)
 exception NoSuchGoals of int
 
-val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
+val tclFOCUS : ?nosuchgoal:'a tactic -> int -> int -> 'a tactic -> 'a tactic
 
 (** [tclFOCUSLIST li t] applies [t] on the list of focused goals
     described by [li]. Each element of [li] is a pair [(i, j)] denoting
@@ -260,13 +258,14 @@ val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
     intervals. If the set of such goals is not a single range, then it
     will move goals such that it is a single range. (So, for
     instance, [[1, 3-5]; idtac.] is not the identity.)
-    If the set of such goals is empty, it will fail. *)
-val tclFOCUSLIST : (int * int) list -> 'a tactic -> 'a tactic
+    If the set of such goals is empty, it will fail with [nosuchgoal],
+    by default raising [NoSuchGoals 0]. *)
+val tclFOCUSLIST : ?nosuchgoal:'a tactic ->  (int * int) list -> 'a tactic -> 'a tactic
 
 (** [tclFOCUSID x t] applies [t] on a (single) focused goal like
     {!tclFOCUS}. The goal is found by its name rather than its
-    number.*)
-val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic
+    number. Fails with [nosuchgoal], by default raising [NoSuchGoals 1]. *)
+val tclFOCUSID : ?nosuchgoal:'a tactic -> Names.Id.t -> 'a tactic -> 'a tactic
 
 (** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the
     specified range doesn't correspond to existing goals, behaves like
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index da3bd41bda..4f36354f79 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -65,13 +65,6 @@ let get_current_context pf =
     let evd = Proof.in_proof p (fun x -> x) in
     evd, Global.env ()
 
-(* Improved error messages *)
-let run_tactic env tac pr =
-  try Proof.run_tactic env tac pr
-  with
-  | Proofview.NoSuchGoals i ->
-    raise Proof_bullet.(SuggestNoSuchGoals(i,pr))
-
 let solve ?with_end_tac gi info_lvl tac pr =
     let tac = match with_end_tac with
       | None -> tac
@@ -80,6 +73,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | None -> tac
       | Some _ -> Proofview.Trace.record_info_trace tac
     in
+    let nosuchgoal = Proofview.tclZERO (Proof_bullet.SuggestNoSuchGoals (1,pr)) in
     let tac = let open Goal_select in match gi with
       | SelectAlreadyFocused ->
         let open Proofview.Notations in
@@ -93,9 +87,9 @@ let solve ?with_end_tac gi info_lvl tac pr =
           in
           Proofview.tclZERO e
 
-      | SelectNth i -> Proofview.tclFOCUS i i tac
-      | SelectList l -> Proofview.tclFOCUSLIST l tac
-      | SelectId id -> Proofview.tclFOCUSID id tac
+      | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
+      | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
+      | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
       | SelectAll -> tac
     in
     let tac =
@@ -104,7 +98,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
       else tac
     in
     let env = Global.env () in
-    let (p,(status,info)) = run_tactic env tac pr in
+    let (p,(status,info)) = Proof.run_tactic env tac pr in
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let () =
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5b77b97988..08b98d702a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -94,13 +94,6 @@ let with_current_proof f (ps, psl) =
   let ps = { ps with proof = newpr } in
   (ps, psl), ret
 
-(* Improved error messages *)
-let with_current_proof f ((ps,_) as pf) =
-  try with_current_proof f pf
-  with
-  | Proofview.NoSuchGoals i ->
-    raise Proof_bullet.(SuggestNoSuchGoals(i,ps.proof))
-
 let simple_with_current_proof f pf =
   let p, () = with_current_proof (fun t p -> f t p , ()) pf in p