diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-05-20 14:06:06 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-05-20 14:06:15 +0200 |
| commit | c1bf3bc4956d0b8af879fcf4854cbd650e1821c0 (patch) | |
| tree | 2bcc2e84f427cf6d6419b56080ef6c4208b595ac /proofs | |
| parent | 9f11adda4bff194a3c6a66d573ce7001d4399886 (diff) | |
Change wrong bullet message.
Remove a space before colon.
Remove the use of term mandatory
(this closes https://coq.inria.fr/bugs/show_bug.cgi?id=3994).
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5f4a7766f..99fab0848 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -516,7 +516,7 @@ module Bullet = struct | NeedClosingBrace -> str"Try unfocusing with \"}\"." | NoBulletInUse -> assert false (* This should never raise an error. *) | ProofFinished -> str"No more subgoals." - | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here." + | Suggest b -> str"Expecting " ++ pr_bullet b ++ str"." | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished." exception FailedBullet of t * suggestion @@ -525,7 +525,7 @@ module Bullet = struct CErrors.register_handler (function | FailedBullet (b,sugg) -> - let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in + let prefix = str"Wrong bullet " ++ pr_bullet b ++ str": " in CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg) | _ -> raise CErrors.Unhandled) |