From e2e4f1388e9ab9dc6a92a9bf9b6c6c001faa048a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 13 Dec 2001 16:42:18 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index e268f14c81..f03e896553 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,7 @@ Language
   the constructors of an inductive types (for compatibility with V6.3
   let-in style)
 - Coercions allowed in Cases patterns
+- Better error messages for ill-typed Cases expressions
 
 Tactics
 
@@ -47,8 +48,10 @@ Bugs
 - Syntax [x:=t:T]u now allowed as mentioned in documentation
 - Various incompatibilities wrt inference of "?" in V6.3.1 fixed
 - Known pattern-matching bugs fixed
+- Known Cases elimination predicate bugs fixed
 - Known coercions bugs
 - Improved errors messages for pattern-matching and projections
+- Implicits in infix section variables bug fixed
 
 ----------------------------------------------------------------------------
 Changes from V6.3.1 and V7.0 to V7.1
-- 
cgit v1.2.3