MAJ

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

1 files changed, 7 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 6cada73db..7781c0bd0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -149,10 +149,13 @@ Library
   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)
-  (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, simpl_plus_l, simpl_le_plus_l; no more
-  implicit arguments in Zmult_Zminus_distr_l and Zmult_Zminus_distr_r)
+  (add_un_double_moins_un_xO, is_double_moins_un),
+  (Rlt_monotony_rev,Rlt_monotony_contra) (source of incompatibilities)
+- Few minor changes (order of arguments of Zsimpl_le_plus_r,
+  Zsimpl_le_plus_l changed, Rge_monotony, Rlt_monotony_contra and
+  Rle_monotony_contra; simpl_plus_l, simpl_le_plus_l; no more implicit
+  arguments in Zmult_Zminus_distr_l and Zmult_Zminus_distr_r, lemmas
+  moved from Zcomplements to other files) (source of incompatibilities)
 - New lemmas provided by users added
 
 Tactic language