From 2def58217686b5083da38778a5ebffb451b1d4d6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 12 Jun 2017 22:12:02 +0200
Subject: [flags] Remove XML output flag.

This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.

It is also not included in the API, so it should either be included in
it or this PR be applied.
---
 lib/flags.ml  | 3 ---
 lib/flags.mli | 5 -----
 2 files changed, 8 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index 0bce22f584..40bad90353 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -87,8 +87,6 @@ let in_toplevel = ref false
 
 let profile = false
 
-let xml_export = ref false
-
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
@@ -96,7 +94,6 @@ let time = ref false
 
 let raw_print = ref false
 
-
 let univ_print = ref false
 
 let we_are_parsing = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index eb4c37a548..388a3ff554 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -56,11 +56,6 @@ val stm_debug : bool ref
 
 val profile : bool
 
-(* Legacy flags *)
-
-(* -xml option: xml hooks will be called *)
-val xml_export : bool ref
-
 (* -ide_slave: printing will be more verbose, will affect stm caching *)
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
-- 
cgit v1.2.3