From 5787cbee1d8ccabd54a52429eb5803b615d7896f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 23 Nov 2003 20:14:53 +0000
Subject: Ajout nouvelles options

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8367 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-com.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex
index ddb39f2422..4f88f600d5 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.
-- 
cgit v1.2.3