diff options
| author | Guillaume Melquiond | 2016-01-02 17:01:28 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-01-02 17:01:28 +0100 |
| commit | 3049b2930ec2bd4adf886fc90bf01a478b318477 (patch) | |
| tree | 00ff808e57abcbc2dcb1775707d26dd9eeba3692 /proofs | |
| parent | 57c7d751df85366ba3781c4e1107a745a660714d (diff) | |
Remove some useless module opening.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5cfec1b0db..8808dbbacd 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -496,10 +496,10 @@ module Bullet = struct | NoBulletInUse -> None | ProofFinished -> None | Suggest b -> Some ("Focus next goal with bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^ Pp.string_of_ppcmds (pr_bullet b) ^".") | Unfinished b -> Some ("The current bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + ^ Pp.string_of_ppcmds (pr_bullet b) ^ " is unfinished.") (* give always a message. *) @@ -508,9 +508,9 @@ module Bullet = struct | NeedClosingBrace -> "Try unfocusing with \"}\"." | NoBulletInUse -> assert false (* This should never raise an error. *) | ProofFinished -> "No more subgoals." - | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (pr_bullet b) ^ " is mandatory here.") - | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) + | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (pr_bullet b) ^ " is not finished.") exception FailedBullet of t * suggestion @@ -519,7 +519,7 @@ module Bullet = struct Errors.register_handler (function | FailedBullet (b,sugg) -> - let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) ^ " : " in + let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (pr_bullet b) ^ " : " in Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg)) | _ -> raise Errors.Unhandled) |