From 4a842a74cfd3fe351c45ebba6733c7a160efa8bf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Mar 2005 15:41:01 +0000
Subject: 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
---
 CHANGES | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 25eb039ff1..ef210416dd 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
 =============================
 
-- 
cgit v1.2.3