Merge branch 'v8.5' into trunk

1 files changed, 5 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 9172195960..050d3e999f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -163,10 +163,11 @@ Specification Language
 - Constructors in pattern-matching patterns now respect the same rules
   regarding implicit arguments than in applicative position. The old
   behavior can be recovered by the command "Set Asymmetric
-  Patterns". As a side effect, Much more notations can be used in
-  patterns. Considering that the pattern language is rich enough like
-  that, definitions are now always forbidden in patterns. (source of
-  incompatibilities for definitions that delta-reduce to a constructor)
+  Patterns". As a side effect, notations for constructors explicitly
+  mentioning non-implicit parameters can now be used in patterns.
+  Considering that the pattern language is already rich enough, binding
+  local definitions is however now forbidden in patterns (source of
+  incompatibilities for local definitions that delta-reduce to a constructor).
 - Type inference algorithm now granting opacity of constants. This might also
   affect behavior of tactics (source of incompatibilities, solvable by
   re-declaring transparent constants which were set opaque).