From 6638997f6c975e88a35ccd260d0c40c287391a45 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 25 Jan 2014 00:15:28 +0100
Subject: More in CHANGES.

---
 CHANGES | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index d1b7327b1d..6ad0f74be8 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
 
-- 
cgit v1.2.3