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.
---
 test-suite/success/ltac.v | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3