From 0b908b3670b7bc19b20af21a0e69b7e732fa854f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 20 Mar 2017 23:58:15 +0100
Subject: [PATCH] Some missing unicode 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 e2f04a721..1951230ad 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -94,19 +94,19 @@ Global Instance from_pure_bupd P Ï† : FromPure P Ï† â†’ FromPure (|==> P) Ï†.
 Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
 
 Global Instance from_pure_pure_and (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure P1 Ï†1 -> FromPure P2 Ï†2 -> FromPure (P1 âˆ§ P2) (Ï†1 âˆ§ Ï†2).
+  FromPure P1 Ï†1 â†’ FromPure P2 Ï†2 â†’ FromPure (P1 âˆ§ P2) (Ï†1 âˆ§ Ï†2).
 Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
 Global Instance from_pure_pure_sep (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure P1 Ï†1 -> FromPure P2 Ï†2 -> FromPure (P1 âˆ— P2) (Ï†1 âˆ§ Ï†2).
+  FromPure P1 Ï†1 â†’ FromPure P2 Ï†2 â†’ FromPure (P1 âˆ— P2) (Ï†1 âˆ§ Ï†2).
 Proof. rewrite /FromPure pure_and always_and_sep_l. by intros -> ->. Qed.
 Global Instance from_pure_pure_or (Ï†1 Ï†2 : Prop) P1 P2 :
-  FromPure P1 Ï†1 -> FromPure P2 Ï†2 -> FromPure (P1 âˆ¨ P2) (Ï†1 âˆ¨ Ï†2).
+  FromPure P1 Ï†1 â†’ FromPure P2 Ï†2 â†’ FromPure (P1 âˆ¨ P2) (Ï†1 âˆ¨ Ï†2).
 Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
 Global Instance from_pure_pure_impl (Ï†1 Ï†2 : Prop) P1 P2 :
-  IntoPure P1 Ï†1 -> FromPure P2 Ï†2 -> FromPure (P1 â†’ P2) (Ï†1 â†’ Ï†2).
+  IntoPure P1 Ï†1 â†’ FromPure P2 Ï†2 â†’ FromPure (P1 â†’ P2) (Ï†1 â†’ Ï†2).
 Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
 Global Instance from_pure_pure_wand (Ï†1 Ï†2 : Prop) P1 P2 :
-  IntoPure P1 Ï†1 -> FromPure P2 Ï†2 -> FromPure (P1 -âˆ— P2) (Ï†1 â†’ Ï†2).
+  IntoPure P1 Ï†1 â†’ FromPure P2 Ï†2 â†’ FromPure (P1 -âˆ— P2) (Ï†1 â†’ Ï†2).
 Proof.
   rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
 Qed.
-- 
GitLab