1 files changed, 3 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index b4d8397e97..c51cbd9dcd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -93,6 +93,8 @@ Libraries (DOC TO CHECK)
 - Slight restructuration of the Logic library regarding choice and classical
   logic. Addition of files providing intuitionistic axiomatizations of
   descriptions: Epsilon.v, Description.v and IndefiniteDescription.v.
+- Definition of pred and minus made compatible with the structural
+  decreasing criterion for use in fixpoints.
 
 Notations, coercions, implicit arguments and type inference
 
@@ -497,7 +499,7 @@ Modules
   "Module Type M(Export/Import X Y: T)"
   (only for interactive definitions)
 - Construct "with" generalized to module paths:
-   T with (Definition|Module) M1.M2....Mn.l := l' (doc TODO).
+   T with (Definition|Module) M1.M2....Mn.l := l'.
 
 Notations