diff options
| -rwxr-xr-x | doc/RefMan-com.tex | 11 |
1 files changed, 11 insertions, 0 deletions
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. |