Ajout nouvelles options

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8367 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 0 deletions

diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex
index ddb39f242..4f88f600d 100755
--- a/doc/RefMan-com.tex
+++ b/doc/RefMan-com.tex
@@ -176,6 +176,17 @@ The following command-line options are recognized by the commands {\tt
   Launch \Coq\ under the Objective Caml debugger (provided that \Coq\
   has been compiled for debugging; see next chapter).
 
+\item[{\tt -impredicative-set}]\ \\
+  Change the logical theory of {\Coq} by declaring the sort {\tt Set}
+  impredicative; warning: this is known to be inconsistent with
+  some standard axioms of classical mathematics such as the functional
+  axiom of choice or the principle of description\\
+
+\item[{\tt -dont-load-proofs}]\ \\
+  This avoids loading in memory the proofs of opaque theorems
+  resulting in a smaller memory requirement and faster compilation;
+  warning: this invalidates some features such as the extraction tool.
+
 \item[{\tt -image} {\em file}]\ \\
   This option sets the binary image to be used to be {\em file}
   instead of the standard one. Not of general use.