diff options
| author | Guillaume Melquiond | 2014-06-13 16:07:46 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2014-06-13 16:08:46 +0200 |
| commit | 505a6a2cb01eea3b4f60b9e9b3b583b56f1bd50b (patch) | |
| tree | a863d2e62e1c4db81c88ed48e4bad71a4a9f20d5 /doc | |
| parent | f8f65b0227056d49dc31174c89ea0da4427e3b56 (diff) | |
Deprecate options -dont, -lazy, -force-load-proofs.
These options no longer have any impact on the way proofs are loaded. In
other words, loading is always lazy, whatever the options. Keeping them
just so that coqc dies when the user prints some opaque symbol does not
seem worth it.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 67cb50c295..172af9730c 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -217,22 +217,6 @@ Section~\ref{LongNames}). This dumps references for global names in file {\em file} (to be used by coqdoc, see~\ref{coqdoc}) -\item[{\tt -dont-load-proofs}]\ - - In this mode, it is an error to access the body of opaque theorems - (for example via {\tt Print} or {\tt Print Assumptions}). - -\item[{\tt -lazy-load-proofs}]\ - - This is the default behavior. Proofs of opaque theorems aren't - loaded immediately in memory, but only when necessary, for instance - during a {\tt Print} or {\tt Print Assumptions}. This mode should be - almost as fast and efficient as {\tt -dont-load-proofs}. - -\item[{\tt -force-load-proofs}]\ - - Deprecated, now the same as {\tt -lazy-load-proofs}. - \item[{\tt -no-hash-consing}] \mbox{} \item[{\tt -vm}]\ |