From 44a669e591ee00bcea65b229429dcb5d4d3515ec Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Apr 2019 00:28:15 +0200
Subject: [native compiler] Fix critical bug with primitive projections

Since e1e7888, stuck projections were not computed correctly.

Fixes #9684
---
 test-suite/bugs/closed/bug_9684.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9684.v

(limited to 'test-suite/bugs')

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.
+*)
-- 
cgit v1.2.3