diff options
Diffstat (limited to 'src/Util/Prod.v')
| -rw-r--r-- | src/Util/Prod.v | 16 |
1 files changed, 8 insertions, 8 deletions
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 *) |