From e8ccf6120f3765e04c527bca8b2b1fffc6df08ca Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Aug 2018 14:59:23 +0200
Subject: Fixing #8270 (cbn was calling zeta even when not asked for).

---
 test-suite/bugs/closed/8270.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/bugs/closed/8270.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/8270.v b/test-suite/bugs/closed/8270.v
new file mode 100644
index 0000000000..f36f757f10
--- /dev/null
+++ b/test-suite/bugs/closed/8270.v
@@ -0,0 +1,15 @@
+(* Don't do zeta in cbn when not asked for *)
+
+Goal let x := 0 in
+     let y := x in
+     y = 0.
+  (* We use "cofix" as an example because there are obviously no
+     cofixpoints in sight.  This problem arises with any set of
+     reduction flags (not including zeta where the lets are of course reduced away) *)
+  cbn cofix.
+  intro x.
+  unfold x at 1. (* Should succeed *)
+  Undo 2.
+  cbn zeta.
+  Fail unfold x at 1.
+Abort.
-- 
cgit v1.2.3