More in CHANGES.

1 files changed, 9 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index d1b7327b1..6ad0f74be 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,13 +14,21 @@ Vernacular commands
   name "Search" now behaves like former "SearchAbout". The latter name
   is deprecated.
 
-Specification Language
+Notations
 
 - The syntax "x -> y" is now declared at level 99. In particular, it has
   now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)"
   (possible source of incompatibilities)
+- Notations accept term-provinding tactics using the $(...)$ syntax.
+
+Specification Language
+
 - Slight changes in unification error messages.
 - Added a syntax $(...)$ allowing to put tactics in terms.
+- Constants in pattern-matching branches now respect the same rules regarding
+  implicit arguments than in applicative position. The old behaviour can be
+  recovered by the command "Set Asymmetric Patterns". (possible source of
+  incompatibilities)
 
 Tactics