Use streams rather than strings to handle bullet suggestions.

1 files changed, 3 insertions, 4 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9ee7df14c8..e01bed5dad 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -353,7 +353,7 @@ 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 nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ())
 let set_nosuchgoals_hook f = nosuchgoals_hook := f
 
 
@@ -361,10 +361,9 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f
 (* This uses the hook above *)
 let _ = Errors.register_handler begin function
   | NoSuchGoals n ->
-    let suffix:string option = (!nosuchgoals_hook) n in
+    let suffix = !nosuchgoals_hook n in
     Errors.errorlabstrm ""
-      (str "No such " ++ str (String.plural n "goal") ++ str "."
-       ++ pr_opt str suffix)
+      (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix)
   | _ -> raise Errors.Unhandled
 end