diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-24 09:38:52 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-24 09:38:52 +0200 |
| commit | cc9618ef7543566013f4c9831df25f9503527507 (patch) | |
| tree | b9ce23a200564ea60b3c5021d7c894ed1063714c | |
| parent | a8401c47b6fd9ff9542dfcd0f31a5e84405c930d (diff) | |
coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".
This prevented the message from being silent when jumping ahead in a file. Fixes #3636.
| -rw-r--r-- | printing/printer.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index c83a9fb04..bb1c2dab9 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -623,10 +623,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = ++ fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> - (* emacs mode: xml-like flag for detecting information message *) - str (emacs_str "<infomsg>") ++ str "This subproof is complete, but there are still unfocused goals." - ++ str (emacs_str "</infomsg>") ++ fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals end |