Missing translating a 'O' into a '0' (again - cf bug #947); removed useless hypothesis of Zlt/Zgt_square_simpl (cg #948)

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

1 files changed, 7 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 25eb039ff..ef210416d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,6 +45,13 @@ Notations
 
 - "format" option aware of recursive notations
 
+Library
+
+- Few 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
+  digit 0)
+
 Changes from V8.0beta to V8.0
 =============================