aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES4
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,