From c1f017d27895df046f467732cda757ab2f76bbef Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 13 May 2002 13:42:40 +0000
Subject: Pas de projection si le nom d'un champ est '_' dans un Record

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

diff --git a/CHANGES b/CHANGES
index 41c2138ef3..974a16a938 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,7 @@ Language
 
 - Slightly improved compilation of pattern-matching (slight source of
   incompatibilities)
+- Record's now accept anonymous fields "_" which does not build projections
 
 Tactics
 
-- 
cgit v1.2.3