diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-22 16:49:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-22 16:49:26 +0000 |
| commit | e8587d7875a0fb1d46541932231602e2326f3492 (patch) | |
| tree | bb03c6ababf445da4f133a73b8cb1aa3bce0c749 /doc | |
| parent | 58b4b442d6815a86d8abe251c421de5dbe206e8f (diff) | |
Ajout option -xml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8478 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rwxr-xr-x | doc/RefMan-com.tex | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex index 34e421149..cf5b100e7 100755 --- a/doc/RefMan-com.tex +++ b/doc/RefMan-com.tex @@ -185,6 +185,11 @@ The following command-line options are recognized by the commands {\tt 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 -emacs}]\ Tells \Coq\ it is executed under Emacs. |