From cc9618ef7543566013f4c9831df25f9503527507 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 24 Sep 2014 09:38:52 +0200
Subject: 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.---
 printing/printer.ml | 3 ---
 1 file changed, 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
-- 
cgit v1.2.3