From 853821e4374050d5a770ee623b24a7bf15e288ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 8 Nov 2016 11:22:11 -0500 Subject: Rename iffT, add some lemmas about tuple and hlist Some lemmas admitted --- src/Util/Prod.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'src/Util/Prod.v') diff --git a/src/Util/Prod.v b/src/Util/Prod.v index fea2589be..bcd9404a6 100644 --- a/src/Util/Prod.v +++ b/src/Util/Prod.v @@ -76,23 +76,23 @@ Proof. repeat (intros [? ?] || intro || split); assumption. Defined. Global Instance iff_prod_Proper : Proper (iff ==> iff ==> iff) (fun A B => prod A B). Proof. repeat intro; tauto. Defined. -Global Instance iff_iffT_prod_Proper - : Proper (iff ==> iffT ==> iffT) (fun A B => prod A B) | 1. +Global Instance iff_iffTp_prod_Proper + : Proper (iff ==> iffTp ==> iffTp) (fun A B => prod A B) | 1. Proof. intros ?? [?] ?? [?]; constructor; tauto. Defined. -Global Instance iffT_iff_prod_Proper - : Proper (iffT ==> iff ==> iffT) (fun A B => prod A B) | 1. +Global Instance iffTp_iff_prod_Proper + : Proper (iffTp ==> iff ==> iffTp) (fun A B => prod A B) | 1. Proof. intros ?? [?] ?? [?]; constructor; tauto. Defined. -Global Instance iffT_iffT_prod_Proper - : Proper (iffT ==> iffT ==> iffT) (fun A B => prod A B) | 1. +Global Instance iffTp_iffTp_prod_Proper + : Proper (iffTp ==> iffTp ==> iffTp) (fun A B => prod A B) | 1. Proof. intros ?? [?] ?? [?]; constructor; tauto. Defined. -Hint Extern 2 (Proper _ prod) => apply iffT_iffT_prod_Proper : typeclass_instances. -Hint Extern 2 (Proper _ (fun A => prod A)) => refine iff_iffT_prod_Proper : typeclass_instances. +Hint Extern 2 (Proper _ prod) => apply iffTp_iffTp_prod_Proper : typeclass_instances. +Hint Extern 2 (Proper _ (fun A => prod A)) => refine iff_iffTp_prod_Proper : typeclass_instances. Hint Extern 2 (Proper _ (fun A B => prod A B)) => refine iff_prod_Proper : typeclass_instances. (** ** Useful Tactics *) -- cgit v1.2.3