MAJ diverses

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

Author: herbelin

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

COMPATIBILITY

@@ -53,7 +53,10 @@ Language
 Libraries
 
 - Some changes in the library (as mentioned in the CHANGES file) may
-  imply the need for local adaptations.
+  imply the need for local adaptations. This may particularly be the
+  case with the move from Set to Type in libraries FSets, SetoidList,
+  ListSet, Sorting and Zmisc. In case of trouble it may help to simply
+  declare Set as an alias for Type (see file SetIsType).
 
 For the main changes in the ML interfaces, see file
 dev/doc/changes.txt in the main archive.

dev/doc/changes.txt

@@ -2,9 +2,14 @@
 = CHANGES BETWEEN COQ V8.1 AND COQ V8.2 =
 =========================================
 
-A few differences in Coq ML interfaces between Coq V8.0 and V8.1
+A few differences in Coq ML interfaces between Coq V8.1 and V8.2
 ================================================================
 
+** Datatypes
+
+List of occurrences moved from "int list" to "Termops.occurrences" (an
+alias to "bool * int list").
+
 ** Functions
 
 Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply