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.
---
 doc/tools/Translator.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/tools/Translator.tex')

diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index ed1d336d9e..3ee65d6f22 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}
 
-- 
cgit v1.2.3

