From 8d1a5297d55eb0cd02695c81f6dea7aef6f62d31 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 19 Apr 2018 14:26:54 +0200
Subject: Made names of existential variables interpretable as Ltac variables.

This concerns e.g. "?[id]", "?[?id]" or "?id" (in terms, not in
patterns), so that all names occurring in terms are consistently
interpreted as ltac names.

Moreover, with that, we can for instance do:

Ltac pick x := eexists ?[x].
Goal exists x, x = 0.
pick foo.
---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index bca4788058..a643e388bf 100644
--- a/CHANGES
+++ b/CHANGES
@@ -59,6 +59,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,
-- 
cgit v1.2.3