diff options
Diffstat (limited to 'printing/printer.ml')
| -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 c83a9fb04f..bb1c2dab95 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 |