diff options
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 926ee986a7..56cf8b06a7 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). |