From 8e79ac5a766e42dfbfc629087455c9bd7639402c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 17 Aug 2016 09:33:03 +0200
Subject: infoH: output via msg_* to make the XML protocol happy

---
 proofs/refiner.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 14493458cf..ef4cfb158d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -218,7 +218,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
 	   (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc)
 	   "" lh))
     "" newhyps in
-  pp (str (emacs_str "<infoH>")
+  msg_notice (str (emacs_str "<infoH>")
       ++  (hov 0 (str s))
       ++  (str (emacs_str "</infoH>")) ++ fnl());
   tclIDTAC goal;;
-- 
cgit v1.2.3