From 8c32ecc205aebaf9a4da95e24463286aee1a571d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 27 Sep 2014 18:42:21 +0200
Subject: Fix bug 3662 by actually reducing primitive projections in
 cbv/compute.

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

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v
new file mode 100644
index 0000000000..0de92b131e
--- /dev/null
+++ b/test-suite/bugs/closed/3662.v
@@ -0,0 +1,47 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Record Elimination Schemes.
+Record prod A B := pair { fst : A ; snd : B }.
+Definition f : Set -> Type := fun x => x.
+
+Goal (fst (pair (fun x => x + 1) nat) 0) = 0.
+compute.
+Undo.
+cbv.
+Undo.
+Opaque fst.
+cbn.
+Transparent fst.
+cbn.
+Undo.
+simpl.
+Undo.
+Abort.
+
+Goal f (fst (pair nat nat)) = nat.
+compute.
+  match goal with
+    | [ |- fst ?x = nat ] => fail 1 "compute failed"
+    | [ |- nat = nat ] => idtac
+  end.
+  reflexivity.
+Defined.
+
+Goal fst (pair nat nat) = nat.
+  unfold fst. 
+  match goal with
+    | [ |- fst ?x = nat ] => fail 1 "compute failed"
+    | [ |- nat = nat ] => idtac
+  end.
+  reflexivity.
+Defined.
+
+Lemma eta A B : forall x : prod A B, x = pair (fst x) (snd x). reflexivity. Qed.
+
+Goal forall x : prod nat nat, fst x = 0.
+  intros. unfold fst. rewrite (eta x). cbv iota. cbv delta. cbv iota.
+  cbv delta. 
+  match goal with
+    | [ |- fst ?x = 0 ] => idtac
+  end.
+Abort.
\ No newline at end of file
-- 
cgit v1.2.3