MAJ diverses

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

1 files changed, 2 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index c2e6c741f3..4304fce184 100644
--- a/CHANGES
+++ b/CHANGES
@@ -20,6 +20,7 @@ Language
 - Support for sort-polymorphism on constants denoting inductive types.
 - Several evolutions of the module system (handling of module aliases, 
   functorial module types, an Include feature, etc). (TODO: Say more!)
+- Prop now a subtype of Set (predicative and impredicative forms).
 
 Vernacular commands
 
@@ -403,7 +404,7 @@ Tools
 Miscellaneous
 
 - Coq installation provides enough files so that Ocaml's extensions need not
-  the Coq sources to be compiled.
+  the Coq sources to be compiled (this assumes O'Caml 3.10 and Camlp5).
 - New commands "Set Whelp Server" and "Set Whelp Getter" to customize the
   Whelp search tool.
 - Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into