diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index e2f04a721c8747c73d62ab9a61fb20448365a5f0..1951230ad43040d06a96e0cde06c45105e932ae8 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.