aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-12 22:12:02 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-08-01 18:42:44 +0200
commit2def58217686b5083da38778a5ebffb451b1d4d6 (patch)
treec0c2463a4620fe3c6bb2caf21a70f6861bbb4643 /doc
parent65bd1deac80689d02be7ef580872974cc38bf93c (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 'doc')
-rw-r--r--doc/tools/Translator.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index ed1d336d9..3ee65d6f2 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -614,7 +614,7 @@ is compiled by a Makefile with the following constraints:
\begin{itemize}
\item compilation is achieved by invoking make without specifying a target
\item options are passed to Coq with make variable COQFLAGS that
- includes variables OPT, COQLIBS, OTHERFLAGS and COQ_XML.
+ includes variables OPT, COQLIBS, and OTHERFLAGS.
\end{itemize}
These constraints are met by the makefiles produced by {\tt coq\_makefile}