From 6b041a242607ec906fbab451e53c15af6339e4ef Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 18 May 2017 07:31:36 +0200
Subject: [emacs] [toplevel] Make emacs flag local to the toplevel.

We remove the emacs-specific printing code from the core of Coq, now
`-emacs` is a printing flag controlled by the toplevel.
---
 proofs/refiner.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 259e96a276..91e6dc4ab2 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -188,8 +188,6 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
       (fun hypl -> List.subtract cmp hypl oldhyps)
       hyps
   in
-  let emacs_str s =
-    if !Flags.print_emacs then s else "" in
   let s = 
     let frst = ref true in
     List.fold_left
@@ -199,9 +197,9 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
 	   "" lh))
     "" newhyps in
   Feedback.msg_notice
-    (str (emacs_str "<infoH>")
+    (str "<infoH>"
       ++  (hov 0 (str s))
-      ++  (str (emacs_str "</infoH>")));
+      ++  (str "</infoH>"));
   tclIDTAC goal;;
 
 
-- 
cgit v1.2.3