From 9ee62a197ea094911907341848d624ba33789f24 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Sat, 28 Feb 2015 15:22:37 +0100
Subject: Explicit in CHANGES incompatibilities introduced in patterns by
 b2953849 (or r15439 as we were talking at that time)

---
 CHANGES | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/CHANGES b/CHANGES
index 712a8a7e92..e44fd5de0c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -83,10 +83,13 @@ Specification Language
 - Added a syntax $(...)$ that allows putting tactics in terms (may
   break user notations using "$(", fixable by inserting a space or
   rewriting the notation).
-- Constants in pattern-matching branches now respect the same rules regarding
-  implicit arguments than in applicative position. The old behavior can be
-  recovered by the command "Set Asymmetric Patterns". (possible source of
-  incompatibilities)
+- 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)
 - 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).
-- 
cgit v1.2.3