Imported Upstream version 8.5~beta1+dfsg

1 files changed, 47 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v
new file mode 100644
index 00000000..bd53389b
--- /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.
+  Fail match goal with
+    | [ |- fst ?x = 0 ] => idtac
+  end.
+Abort.
+