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.

1 files changed, 4 insertions, 0 deletions

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,