diff options
| author | Emilio Jesus Gallego Arias | 2017-06-12 22:12:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-08-01 18:42:44 +0200 |
| commit | 2def58217686b5083da38778a5ebffb451b1d4d6 (patch) | |
| tree | c0c2463a4620fe3c6bb2caf21a70f6861bbb4643 /man | |
| 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 'man')
| -rw-r--r-- | man/coqide.1 | 7 | ||||
| -rw-r--r-- | man/coqtop.1 | 6 |
2 files changed, 0 insertions, 13 deletions
diff --git a/man/coqide.1 b/man/coqide.1 index f82bf2ad40..3592f6e4e3 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -123,13 +123,6 @@ Set sort Set impredicative. .TP .B \-dont\-load\-proofs Don't load opaque proofs in memory. -.TP -.B \-xml -Export XML files either to the hierarchy rooted in -the directory -.B COQ_XML_LIBRARY_ROOT -(if set) or to stdout (if unset). - .SH SEE ALSO diff --git a/man/coqtop.1 b/man/coqtop.1 index feee7fd8b5..62d17aa674 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -153,12 +153,6 @@ set sort Set impredicative .B \-dont\-load\-proofs don't load opaque proofs in memory -.TP -.B \-xml -export XML files either to the hierarchy rooted in -the directory $COQ_XML_LIBRARY_ROOT (if set) or to -stdout (if unset) - .SH SEE ALSO .BR coqc (1), |