From fde155742bf2dabc08dff82ef3a1bbbb676c8c4b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 26 Apr 2005 16:42:06 +0000
Subject: Fixed hypotheses of Z_lt_induction (see #957)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6962 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index ef210416dd..45c5d671ce 100644
--- a/CHANGES
+++ b/CHANGES
@@ -50,7 +50,7 @@ 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)
+  digit 0; weaken premises in Z_lt_induction)
 
 Changes from V8.0beta to V8.0
 =============================
-- 
cgit v1.2.3