Test for #4035 (dependent destruction from Ltac).

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4035.v b/test-suite/bugs/closed/4035.v
new file mode 100644
index 0000000000..ec246d097b
--- /dev/null
+++ b/test-suite/bugs/closed/4035.v
@@ -0,0 +1,13 @@
+(* Supporting tactic notations within Ltac in the presence of an
+  "ident" entry which does not expect a fresh ident *)
+(* Of course, this is a matter of convention of what "ident" is
+   supposed to denote, but in practice, it seems more convenient to
+   have less constraints on ident at interpretation time, as
+   otherwise more ad hoc entries would be necessary (as e.g. a special
+   "quantified_hypothesis" entry for dependent destruction). *)
+Require Import Program.
+Goal nat -> Type.
+  intro x.
+  lazymatch goal with
+  | [ x : nat |- _ ] => dependent destruction x
+  end.