diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 4557f7908d4e1669e2ac714f2a40fd706082ef8c..a449d7d498fa024cb66f3e2c09678b3122f74c82 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -43,13 +43,13 @@ Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
   @IntoPure M (âœ“ a) (âœ“ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
-Global Instance into_pure_pure_conj (Ï†1 Ï†2 : Prop) P1 P2 :
+Global Instance into_pure_pure_and (Ï†1 Ï†2 : Prop) P1 P2 :
   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).
 Proof. rewrite /IntoPure sep_and pure_and. by intros -> ->. Qed.
-Global Instance into_pure_pure_disj (Ï†1 Ï†2 : Prop) P1 P2 :
+Global Instance into_pure_pure_or (Ï†1 Ï†2 : Prop) P1 P2 :
   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 :
@@ -91,13 +91,13 @@ Qed.
 Global Instance from_pure_bupd P Ï† : FromPure P Ï† â†’ FromPure (|==> P) Ï†.
 Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
 
-Global Instance from_pure_pure_conj (Ï†1 Ï†2 : Prop) P1 P2 :
+Global Instance from_pure_pure_and (Ï†1 Ï†2 : Prop) P1 P2 :
   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).
 Proof. rewrite /FromPure pure_and always_and_sep_l. by intros -> ->. Qed.
-Global Instance from_pure_pure_disj (Ï†1 Ï†2 : Prop) P1 P2 :
+Global Instance from_pure_pure_or (Ï†1 Ï†2 : Prop) P1 P2 :
   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 :