diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index a449d7d498fa024cb66f3e2c09678b3122f74c82..990410360c0f5a95d51adef8e946bbc386088683 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.