From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- 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/closed/3662.v') 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. + -- cgit v1.2.3