Merge PR #7309: Made names of existential variables interpretable as Ltac variables.

1 files changed, 4 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 29b8fa1094..9f3bdcedae 100644
--- a/CHANGES
+++ b/CHANGES
@@ -73,6 +73,10 @@ Tactics
 
 - The `romega` tactics have been deprecated; please use `lia` instead.
 
+- Names of existential variables occurring in Ltac functions
+  (e.g. "?[n]" or "?n" in terms - not in patterns) are now interpreted
+  the same way as other variable names occurring in Ltac functions.
+
 Focusing
 
 - Focusing bracket `{` now supports named goal selectors,