Merge PR #9900: [native compiler] Fix critical bug with stuck primitive projections

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_9684.v b/test-suite/bugs/closed/bug_9684.v
new file mode 100644
index 0000000000..436a00585b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9684.v
@@ -0,0 +1,19 @@
+Set Primitive Projections.
+
+Record foo := mkFoo { proj1 : bool; proj2 : bool }.
+
+Definition x := mkFoo true false.
+Definition proj x := proj2 x.
+
+Lemma oops : proj = fun x => proj1 x.
+Proof. Fail native_compute; reflexivity. Abort.
+
+(*
+Lemma bad : False.
+assert (proj1 x = proj x).
+  rewrite oops; reflexivity.
+discriminate.
+Qed.
+
+Print Assumptions bad.
+*)