Merge PR #8285: Fixing #8270: cbn was applying zeta even when not asked for.

1 files changed, 15 insertions, 0 deletions

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.