diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/tools/Translator.tex | 2 |
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} |