Merge PR #10899: Fixes #10894 regression: uconstr was not anymore typed in the Ltac-substituted environment

Reviewed-by: ejgallego
Reviewed-by: ppedrot

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_10894.v b/test-suite/bugs/closed/bug_10894.v
new file mode 100644
index 0000000000..b8c9367951
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10894.v
@@ -0,0 +1,12 @@
+(* Check that uconstrs are interpreted in the ltac-substituted environment *)
+(* Was a regression introduced in 4dab4fc (#7288) *)
+
+Tactic Notation "bind" hyp(x) "in" uconstr(f) "as" ident(h) :=
+   set (h := fun x => f).
+
+Fact test : nat -> nat.
+Proof.
+  intros n.
+  bind n in (n*n) as f.
+  assert (f 0 = 0) by reflexivity.
+Abort.