diff options
| author | Emilio Jesus Gallego Arias | 2017-02-22 02:08:29 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-12 16:49:46 +0200 |
| commit | 46856a80958f1aaa3242b6d37f018df9528e5e5f (patch) | |
| tree | 3c15b53a6f6ff36629e7fbff317ee73cc9ed818f /ide | |
| parent | ce2b2058587224ade9261cd4127ef4f6e94d356b (diff) | |
[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.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 3 |
1 files changed, 0 insertions, 3 deletions
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 |