From 8858c1a06eccc5d2f32b43bdda6fc1083d9cf4f0 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 8 Sep 2014 09:51:11 +0200
Subject: CHANGES: binder names from Ltac identifiers.

---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGES b/CHANGES
index 18c5a53508..fc111d211d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -172,6 +172,8 @@ Tactics
   (possible source of incompatibilities solvable by avoiding clearing
   the relevant hypotheses).
 - New construct "uconstr:c" and "type_term c" to build untyped terms.
+- Binders in terms defined in Ltac (either "constr" or "uconstr") can
+  now take their names from identifier defined in Ltac.
 - New bullets --, ++, **, ---, +++, ***, ... made available.
 - The good bullet is suggested sometimes when user gives a wrong one.
 - New tactic "enough", symmetric to "assert", but with subgoals
-- 
cgit v1.2.3