From 8a71148e8068c67c5b7d9b9b0f00ab5de5bf03b7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 30 Jun 2015 16:59:19 +0200
Subject: More precise rewording about asymmetric patterns.

---
 CHANGES | 9 +++++----
 1 file 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).
-- 
cgit v1.2.3