modifs ZArith & Chinese

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

1 files changed, 14 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index e8fd37a0b8..2cd576a702 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,20 @@ Bugs
 - "Intros H" now working like "Intro H" trying first to reduce if not a product
 - Forward dependencies in Cases now taken into account
 
+Standard library
+
+- Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v and Zlogarithms.v)
+  moved from contrib/omega in order to be more visible, one Zsgn function, 
+  more induction principles (Wf_Z.v and tail of Zcomplements.v), 
+  one more general Euclid theorem. 
+
+User Contributions
+
+- Chinese has been rewritten using Z from ZArith as datatype. 
+  ZChinese is the new version, Chinese the obsolete one.   
+
+
+
 
 Changes from V7.1 to V7.2
 =========================