From 5ba84979df97996cd04f44e506742bb58ecf0465 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 16 Dec 2014 14:13:59 +0100
Subject: msg_info now puts infomsg tag in emacs mode.

Fixes the idtac "string" not appearing in proofgeneral because
printined *before* the goal.
---
 proofs/logic_monad.ml | 2 +-
 proofs/refiner.ml     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index 5bad5f0f52..b9c850840d 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -95,7 +95,7 @@ struct
   let print_char = fun c -> (); fun () -> print_char c
 
   (** {!Pp.pp}. The buffer is also flushed. *)
-  let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e ->
+  let print = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e ->
     let (e, info) = Errors.push e in raise ~info e ()
 
   let timeout = fun n t -> (); fun () ->
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index e443ce0772..ea35946102 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -57,7 +57,7 @@ let tclIDTAC gls = goal_goal_list gls
 
 (* the message printing identity tactic *)
 let tclIDTAC_MESSAGE s gls =
-  pp (hov 0 s); pp_flush (); tclIDTAC gls
+  Pp.msg_info (hov 0 s); pp_flush (); tclIDTAC gls
 
 (* General failure tactic *)
 let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
-- 
cgit v1.2.3