From fe815efb9a4681734977e9359b02b4e66f336f49 Mon Sep 17 00:00:00 2001
From: mohring
Date: Tue, 14 May 2002 14:30:52 +0000
Subject: Ajout de la modification des sortes d'elimination

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

diff --git a/CHANGES b/CHANGES
index 974a16a938..b1c7fee435 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,14 @@ Language
 - Slightly improved compilation of pattern-matching (slight source of
   incompatibilities)
 - Record's now accept anonymous fields "_" which does not build projections
+- Changes in the allowed elimination sorts for certain class of 
+inductive definitions :
+	An inductive definition without constructors of Sort Prop can 
+be eliminated on sorts Set and Type
+	A "singleton" inductive definition (one constructor with arguments 
+in the sort Prop like conjunction of two propositions or equality) 
+can be eliminated directly on sort Type (In V7.2, only the sorts Prop and 
+Set were allowed)
 
 Tactics
 
-- 
cgit v1.2.3