From 840155eafd9607c7656c80770de1e2819fe56a13 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 6 Oct 2015 13:38:15 +0200
Subject: Fixing emacs output in debugging mode.

Goal displaying during Debugging ltac is a notice message now. Other
messages are debug messages. This does not change anything in coqide
or coqtop, but allows proofgeneral to dispatch them in the right
buffers (pg had to be fixed too).
---
 proofs/tactic_debug.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'proofs/tactic_debug.ml')

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index d7f4b5ead5..667765dbf2 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -32,7 +32,8 @@ let explain_logic_error = ref (fun e -> mt())
 
 let explain_logic_error_no_anomaly = ref (fun e -> mt())
 
-let msg_tac_debug s = Proofview.NonLogical.print (s++fnl())
+let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
+let msg_tac_notice s = Proofview.NonLogical.print (s++fnl())
 
 (* Prints the goal *)
 
@@ -48,7 +49,7 @@ let db_pr_goal gl =
 let db_pr_goal =
   Proofview.Goal.nf_enter begin fun gl ->
   let pg = db_pr_goal gl in
-  Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg))
+  Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
   end
 
 
-- 
cgit v1.2.3