Intgration uniforme de coercions dans les dclarations (Variable and co) et retouche des Record

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2747 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 81d1a59e2..78edfd6e2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,7 @@ Language
 
 - Inductive definitions now accept ">" in constructor types to declare
   the corresponding constructor as a coercion.
+- Idem for assumptions declarations and constants when the type is mentionned.
 
 ML tactic and vernacular commands