diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-12 22:12:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-08-01 18:42:44 +0200 |
| commit | 2def58217686b5083da38778a5ebffb451b1d4d6 (patch) | |
| tree | c0c2463a4620fe3c6bb2caf21a70f6861bbb4643 /lib | |
| parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) | |
[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.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flags.ml | 3 | ||||
| -rw-r--r-- | lib/flags.mli | 5 |
2 files changed, 0 insertions, 8 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 0bce22f58..40bad9035 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 eb4c37a54..388a3ff55 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 |