1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 704a1d5e34..a4044243d3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -142,6 +142,9 @@ Tactics
   e.g. as argument of a try or a repeat and in a ltac function);
   version of apply that does not unfold is renamed into "simple apply"
   (usable for compatibility or for automation).
+- Tactic apply now able to traverse conjunctions and to select the first 
+  matching lemma among the components of the conjunction; tactic apply also
+  able to apply lemmas of conclusion an empty type.
 - Pattern for hypotheses types in match goal are now interpreted in type_scope.
 
 Type Classes