From ba714f5a7b0930ed538ed52e4058fa3f17bbf871 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 15 Feb 2017 19:38:52 +0100 Subject: [PATCH] fix arrows --- theories/proofmode/class_instances.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v index a449d7d49..990410360 100644 --- a/theories/proofmode/class_instances.v +++ b/theories/proofmode/class_instances.v @@ -44,19 +44,19 @@ Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) : Proof. by rewrite /IntoPure discrete_valid. Qed. Global Instance into_pure_pure_and (φ1 φ2 : Prop) P1 P2 : - IntoPure P1 φ1 -> IntoPure P2 φ2 -> IntoPure (P1 ∧ P2) (φ1 ∧ φ2). + IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∧ P2) (φ1 ∧ φ2). Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed. Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 : - IntoPure P1 φ1 -> IntoPure P2 φ2 -> IntoPure (P1 ∗ P2) (φ1 ∧ φ2). + IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∗ P2) (φ1 ∧ φ2). Proof. rewrite /IntoPure sep_and pure_and. by intros -> ->. Qed. Global Instance into_pure_pure_or (φ1 φ2 : Prop) P1 P2 : - IntoPure P1 φ1 -> IntoPure P2 φ2 -> IntoPure (P1 ∨ P2) (φ1 ∨ φ2). + IntoPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 ∨ P2) (φ1 ∨ φ2). Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed. Global Instance into_pure_pure_impl (φ1 φ2 : Prop) P1 P2 : - FromPure P1 φ1 -> IntoPure P2 φ2 -> IntoPure (P1 → P2) (φ1 → φ2). + FromPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 → P2) (φ1 → φ2). Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed. Global Instance into_pure_pure_wand (φ1 φ2 : Prop) P1 P2 : - FromPure P1 φ1 -> IntoPure P2 φ2 -> IntoPure (P1 -∗ P2) (φ1 → φ2). + FromPure P1 φ1 → IntoPure P2 φ2 → IntoPure (P1 -∗ P2) (φ1 → φ2). Proof. rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->. Qed. -- GitLab