ajout d'une elimination simplifiée Acc_iter pour Acc

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

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 4f62bd10c..a7c253577 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,8 @@ A revision of the standard library and of concrete syntax of Coq, including
   and new eqT is syntactic sugar for new eq (notation == is an alias
   for = and is written as it)
 - similarly, ex, ex2 and all are merged with exT, exT2 and allT.
+- a additional elimination Acc_iter for Acc, simplier than Acc_rect. 
+  This new elimination principle is used for definition well_founded_induction.
 
 Vernacular commands