From 626b27bd1955c1a071d607fbf35706155df5e229 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 10 Oct 2003 19:12:53 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index 5bbb723dba..e324325eda 100644
--- a/CHANGES
+++ b/CHANGES
@@ -107,12 +107,18 @@ Tactics
   arguments (e.g. the accessibility predicate) has been fixed (source
   of incompatibilities)
 - Symmetry now applies to hypotheses too
+- Inversion now accept a "as [ ... ]" option to name the hypotheses
 
 Bugs
 
 - Rename bug fixed (#244)
 - see coq-bugs server for the complete list of fixed bugs
 
+Miscellaneous
+
+- Implicit parameters of inductive types definition now taken into
+  account for infering other implicit arguments
+
 Changes from V7.3.1 to V7.4
 ===========================
 
-- 
cgit v1.2.3