From 424c682a1f9d2dfcac28318bc38c4602c180f5dc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Oct 2017 12:24:29 +0200
Subject: Fixing #2881 ("change with" failing in an Ltac definition).

We fix by interpreting the pattern in "change pat with term" in strict
mode by using the same interning code as for "match goal" (even if the
pattern is dropped afterwards).
---
 test-suite/bugs/closed/2881.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/2881.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2881.v b/test-suite/bugs/closed/2881.v
new file mode 100644
index 0000000000..b4f09305b4
--- /dev/null
+++ b/test-suite/bugs/closed/2881.v
@@ -0,0 +1,7 @@
+(* About scoping of pattern variables in strict/non-strict mode *)
+
+Ltac eta_red := change (fun a => ?f0 a) with f0.
+Goal forall T1 T2 (f : T1 -> T2), (fun x => f x) = f.
+intros.
+eta_red.
+Abort.
-- 
cgit v1.2.3