From f8e8ffa4b7c42f6c53126d284c0bfbf8a992bc89 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sun, 3 Apr 2011 15:18:56 +0000
Subject: 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
---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

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
-- 
cgit v1.2.3