[proof] Fix proof bullet error helper which was implemented as a hook

We add the information on the proper layer by catching the low-level
exception.

2 files changed, 3 insertions, 15 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 316f02bc37..86dcb8ab3b 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -345,22 +345,11 @@ let tclBREAK = Proof.break
 
 exception NoSuchGoals of int
 
-(* This hook returns a string to be appended to the usual message.
-   Primarily used to add a suggestion about the right bullet to use to
-   focus the next goal, if applicable. *)
-let nosuchgoals_hook:(int -> Pp.t) ref = ref (fun n -> mt ())
-let set_nosuchgoals_hook f = nosuchgoals_hook := f
-
-
-
-(* This uses the hook above *)
 let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
-    let suffix = !nosuchgoals_hook n in
-    CErrors.user_err 
-      (str "No such " ++ str (String.plural n "goal") ++ str "." ++
-       pr_non_empty_arg (fun x -> x) suffix)
-      | _ -> raise CErrors.Unhandled
+    CErrors.user_err
+      (str "No such " ++ str (String.plural n "goal") ++ str ".")
+  | _ -> raise CErrors.Unhandled
 end
 
 (** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where
diff --git a/engine/proofview.mli b/engine/proofview.mli
index c772525c86..8685430c62 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -250,7 +250,6 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
     This hook is used to add a suggestion about bullets when
     applicable. *)
 exception NoSuchGoals of int
-val set_nosuchgoals_hook: (int -> Pp.t) -> unit
 
 val tclFOCUS : int -> int -> 'a tactic -> 'a tactic