Update documentation concerning proofs loading (cf last commit)

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

2 files changed, 22 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 0054e4cef6..19edf585e8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -75,6 +75,9 @@ Libraries
 
 Internal infrastructure
 
+- Opaque proofs are now loaded lazily by default. This allows to be almost as
+  fast as -dont-load-proofs, while being safer (no creation of axioms) and
+  avoiding feature restrictions (Print and Print Assumptions work ok).
 - Experimental support added for camlp4 (the one provided alongside ocaml),
   simply pass option -usecamlp4 to ./configure. By default camlp5 is used.
 - Revised build system: no more stages in Makefile thanks to some recursive
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index f808047b12..aaa962570b 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -265,9 +265,25 @@ The following command-line options are recognized by the commands {\tt
  
 \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.
+  Warning: this is an unsafe mode.
+  Instead of loading in memory the proofs of opaque theorems, they are
+  treated as axioms. This results in smaller memory requirement and
+  faster compilation, but the behavior of the system might slightly change
+  (for instance during module subtyping), and some features won't be
+  available (for example {\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 some module subtyping or {\tt Print Assumptions}. This should be
+  almost as fast and efficient as {\tt -dont-load-proofs}, with none
+  of its drawbacks.
+
+\item[{\tt -force-load-proofs}]\
+
+  Proofs of opaque theorems are loaded in memory as soon as the
+  corresponding {\tt Require} is done. This used to be Coq's default behavior.
 
 \item[{\tt -vm}]\