From 259252f2d9477cd721a4a2ad29f9a6fde2bd01ca Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 May 2006 22:08:06 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index e9d0c02652..ea02f78e25 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,10 @@
-Changes from V8.0
-=================
+Changes from V8.0 to V8.1
+=========================
+
+Logic
+
+- Added sort-polymorphism on inductive families
+- Allowance for recursively non uniform parameters in inductive types
 
 Syntax
 
@@ -134,6 +139,7 @@ Libraries
   compatibility (useless hypothesys of Zgt_square_simpl and
   Zlt_square_simpl removed; fixed names mentioning letter O instead of
   digit 0; weaken premises in Z_lt_induction)
+- Restructuration of Eqdep_dec.v and Eqdep.v: more lemmas in Type.
 - Znumtheory now contains a gcd function that can compute within Coq
 - More lemmas stated on Type in Wf.v, removal of redundant Fix_F
 - Coq.List.In_dec has been set transparent (this may exceptionally break
-- 
cgit v1.2.3