Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the

opportunity to extend the class of singleton types to (possibly mutual)
recursive types with single constructors of which all arguments are in
Prop. This covers Acc. Acc_rect can consequently be defined in the
direct way.



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

1 files changed, 6 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 48a7a3682..86f197c61 100644
--- a/CHANGES
+++ b/CHANGES
@@ -28,6 +28,12 @@ Language
 - Several evolutions of the module system (handling of module aliases, 
   functorial module types, an Include feature, etc). (TODO: Say more!)
 - Prop now a subtype of Set (predicative and impredicative forms).
+- Recursive inductive types in Prop with a single constructor of which
+  all arguments are in Prop is now considered to be a singleton
+  type. It consequently supports all eliminations to Prop, Set and Type.
+  As a consequence, Acc_rect has now a more direct proof [possible source
+  of easily fixed incompatibility in case of manual definition of a recursor
+  in a recursive singleton inductive type].
 
 Vernacular commands