From e860dcf1df4d7042aa872ba4ad914d1d64d574cf Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 3 Jun 2002 10:28:40 +0000
Subject: 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
---
 CHANGES | 1 +
 1 file changed, 1 insertion(+)

(limited to 'CHANGES')

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
 
-- 
cgit v1.2.3