diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-25 12:24:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-30 21:12:32 +0100 |
| commit | 424c682a1f9d2dfcac28318bc38c4602c180f5dc (patch) | |
| tree | 6968d6c2c29946ea651c60d2ef3a1548dee4451a /test-suite/bugs/closed/2881.v | |
| parent | ad973248998da8d7d10ed00f4bcd6f383ba9a171 (diff) | |
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).
Diffstat (limited to 'test-suite/bugs/closed/2881.v')
| -rw-r--r-- | test-suite/bugs/closed/2881.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2881.v b/test-suite/bugs/closed/2881.v new file mode 100644 index 000000000..b4f09305b --- /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. |