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. --- man/coqide.1 | 7 ------- man/coqtop.1 | 6 ------ 2 files changed, 13 deletions(-) (limited to 'man') diff --git a/man/coqide.1 b/man/coqide.1 index f82bf2ad4..3592f6e4e 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 feee7fd8b..62d17aa67 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), -- cgit v1.2.3