Fixed and extend bullet related info/error messages. + doc.

Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.

1 files changed, 15 insertions, 1 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index f1d10bbe55..44bf652125 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -343,8 +343,22 @@ let tclBREAK = Proof.break
 (** {7 Focusing tactics} *)
 
 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 -> string option) ref = ref ((fun n -> None))
+let set_nosuchgoals_hook f = nosuchgoals_hook := f
+
+
+
+(* This uses the hook above *)
 let _ = Errors.register_handler begin function
-  | NoSuchGoals n -> Errors.error ("No such " ^ String.plural n "goal" ^".")
+  | NoSuchGoals n ->
+    let suffix:string option = (!nosuchgoals_hook) n in
+    Errors.errorlabstrm ""
+      (str "No such " ++ str (String.plural n "goal") ++ str "."
+       ++ pr_opt str suffix)
   | _ -> raise Errors.Unhandled
 end