diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 18:42:21 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 20:41:05 +0200 |
commit | 8c32ecc205aebaf9a4da95e24463286aee1a571d (patch) | |
tree | b882969507a8ea3262c8fbe14d9f89dfed78817a /test-suite/bugs/closed/3662.v | |
parent | 2dfeec2d73b1fce0d3a461d2215b1a3f65881c9b (diff) |
Fix bug 3662 by actually reducing primitive projections in cbv/compute.
Diffstat (limited to 'test-suite/bugs/closed/3662.v')
-rw-r--r-- | test-suite/bugs/closed/3662.v | 47 |
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 000000000..0de92b131 --- /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 |