From d856e6ea6366e148b9b215fc1ef9631c1da07320 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 22 Oct 2014 10:55:52 +0200
Subject: CHANGES: makes explicit the incompatibily introduced by the use of
 Ltac-defined names in term binders.

Closes #3747.---
 CHANGES | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index b8d7039795..26df1c13b1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -185,7 +185,10 @@ Tactics
   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.
+  now take their names from identifier defined in Ltac. As a
+  consequence, a name cannot be used in a binder (constr:(fun x =>
+  ...)) if an Ltac variable of that name already exists and does not
+  contain an identifier. Source of occasional incompatibilities.
 - The "refine" tactic now accepts untyped terms built with "uconstr"
   so that terms with holes can be constructed piecewise in Ltac.
 - New bullets --, ++, **, ---, +++, ***, ... made available.
-- 
cgit v1.2.3