From 2afbdd7b229eef8f4ee15363bedf84cd087d4257 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Nov 2001 17:51:28 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index 11c000020f..c7ef7f3ebd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,6 +45,8 @@ Bugs
 - Confusion between implicit args of locals and globals of same base name fixed
 - NatRing works (to check)
 - "Discriminate 1", "Injection 1", "Simplify_eq 1" now working
+- NewInduction bugs with let-in and recursively dependent hypotheses fixed
+- 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 coercions bugs
-- 
cgit v1.2.3