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, 27 insertions, 0 deletions

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 4404ff3f16..448febed25 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -377,3 +377,30 @@ f y true.
 Abort.
 
 End LtacNames.
+
+(* Test binding of the name of existential variables in Ltac *)
+
+Module EvarNames.
+
+Ltac pick x := eexists ?[x].
+Goal exists y, y = 0.
+pick foo.
+[foo]:exact 0.
+auto.
+Qed.
+
+Ltac goal x := refine ?[x].
+
+Goal forall n, n + 0 = n.
+Proof.
+  induction n; [ goal Base | goal Rec ].
+  [Base]: {
+    easy.
+  }
+  [Rec]: {
+    simpl.
+    now f_equal.
+  }
+Qed.
+
+End EvarNames.