From 46856a80958f1aaa3242b6d37f018df9528e5e5f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Feb 2017 02:08:29 +0100
Subject: [vernac] vernacentries.mli cleanup

This header file had accumulated quite a bit of cruft over the
years, we clean it up while we are at it.

No functional change as all the removed variables/methods were noops
long time ago.
---
 ide/ide_slave.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index bc7ce38836..65eececf7f 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -466,9 +466,6 @@ let loop () =
   let xml_ic        = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
   let () = Xml_parser.check_eof xml_ic false in
   ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));
-  (* We'll handle goal fetching and display in our own way *)
-  Vernacentries.enable_goal_printing := false;
-  Vernacentries.qed_display_script := false;
   while not !quit do
     try
       let xml_query = Xml_parser.parse xml_ic in
-- 
cgit v1.2.3