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

1 files changed, 8 insertions, 0 deletions

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