Adding ability to put any pattern in binders, prefixed by a quote.

Cf CHANGES for details.

1 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index e90d3d105..0f0a7a04b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,9 @@ Specification language
 - Giving implicit arguments explicitly to a constant with multiple
   choices of implicit arguments does not break any more insertion of
   further maximal implicit arguments.
+- Ability to put any pattern in binders, prefixed by quote, e.g.
+  "fun '(a,b) => ...", "λ '(a,(b,c)), ...", "Definition foo '(x,y) := ...".
+  It expands into a "let 'pattern := ..."
 
 Tactics