diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 7 |
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 |