MAJ

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

1 files changed, 4 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index a402311c2..a9975070b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -58,6 +58,7 @@ Known problems of the automatic translation
 
 - Renaming in ZArith: incompatibilities in Coq user contribs due to
   merging names INZ, from Reals, and inject_nat.
+- Renaming and new lemmas in ZArith: may clash with names used by users
 - Restructuration of ZArith: replace requirement of specific modules
   in ZArith by "Require Import ZArith_base" or "Require Import ZArith"
 - Some implicit arguments must be made explicit before translation: typically
@@ -66,6 +67,7 @@ Known problems of the automatic translation
   new scheme for syntactic extensions (see translator documentation)
 - Unsafe for annotation Cases when constructors coercions are used or when
   annotations are eta-reduced predicates
+ 
 
 Changes from V7.4 to V8.0 old syntax
 ====================================
@@ -144,8 +146,8 @@ Library
   - Redundant ZArith lemmas have been renamed: for the following pairs,
   use the second name (Zle_Zmult_right2, Zle_mult_simpl), (OMEGA2,
   Zle_0_plus), (Zplus_assoc_l, Zplus_assoc), (Zmult_one, Zmult_1_n),
-  (Zmult_assoc_l, Zmult_assoc), (Zmult_minus_distr,
-  Zmult_Zminus_distr_l) (source of incompatibilities)
+  (Zmult_assoc_l, Zmult_assoc), (Zmult_minus_distr, Zmult_Zminus_distr_l)
+  (add_un_double_moins_un_xO, is_double_moins_un) (source of incompatibilities)
 - Few minor changes (order of arguments of Zsimpl_le_plus_r and
   Zsimpl_le_plus_l changed; no more implicit arguments in
   Zmult_Zminus_distr_l and Zmult_Zminus_distr_r)