diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-11 11:52:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-11 11:52:00 +0200 |
| commit | 691d62a306fe072f0d91ff665a73c29400adfde4 (patch) | |
| tree | e64260679186d196255b5863fbf1be12a6ac66d4 /doc/refman/RefMan-com.tex | |
| parent | bcd144642c5f23a69ac96afe3a9f3ae370fcfa96 (diff) | |
Removing remaining documentation of the XML plugin.
Diffstat (limited to 'doc/refman/RefMan-com.tex')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 926ee986a..56cf8b06a 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -172,11 +172,6 @@ Add physical path {\em directory} to the {\ocaml} loadpath. % % Switch on the debug flag. -\item[{\tt -xml}]\ - - This option is for use with {\tt coqc}. It tells \Coq\ to export on - the standard output the content of the compiled file into XML format. - \item[{\tt -with-geoproof} (yes|no)]\ Activate or not special functions for Geoproof within {\CoqIDE} (default is yes). |