MAJ

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

1 files changed, 5 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 97c02e6c71..a8494e47a3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -3,9 +3,12 @@ Changes from V8.1beta to V8.1
 
 - Support for Miller-Pfenning's patterns unification in type synthesis
   (e.g. can infer P such that P x y = phi(x,y))
+- Support for implicit arguments in the types of parameters in
+  (co-)fixpoints and (co-)inductive declarations
+- Support for "where" clause in cofixpoint definitions
 
-Changes from V8.0 to V8.1
-=========================
+Changes from V8.0 to V8.1beta
+=============================
 
 Logic