MAJ

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

1 files changed, 7 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 61e3e838ba..f4b6751053 100644
--- a/CHANGES
+++ b/CHANGES
@@ -134,8 +134,8 @@ Libraries
 - New library FSets+FMaps of finite sets and maps.
 - New library QArith on rational numbers.
 - Small extension of Zmin.V, new Zmax.v, new Zminmax.v.
-- Reworking of the files on classical logic and description principles
-  (possible incompatibilities).
+- Reworking and extension of the files on classical logic and
+  description principles (possible incompatibilities)
 - Few other improvements in ZArith potentially exceptionally breaking the
   compatibility (useless hypothesys of Zgt_square_simpl and
   Zlt_square_simpl removed; fixed names mentioning letter O instead of
@@ -144,6 +144,11 @@ Libraries
 - Znumtheory now contains a gcd function that can compute within Coq.
 - More lemmas stated on Type in Wf.v, removal of redundant Fix_F.
 - Change of the internal names of lemmas in OmegaLemmas.
+- Acc in Wf.v and clos_refl_trans in Relation_Operators.v now rely on
+  the allowance for recursively non uniform parameters (possible
+  source of incompatibilities: explicit pattern-matching on these
+  types may require to remove the occurrence associated to their
+  recursively non uniform parameter).
 - Coq.List.In_dec has been set transparent (this may exceptionally break
   proof scripts, set it locally opaque for compatibility).
 - More on permutations of lists in List.v and Permutation.v.