diff --git a/theories/option.v b/theories/option.v
index 412cd5ce1c09b69bc6041e9cdbfd138cda585499..28ecff3be420afe1c2db9b74ee6834ddecf94eff 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -243,10 +243,10 @@ Proof. by destruct mx. Qed.
 Global Instance option_fmap_proper `{Equiv A, Equiv B} :
   Proper (((â‰¡) ==> (â‰¡)) ==> (â‰¡@{option A}) ==> (â‰¡@{option B})) fmap.
 Proof. destruct 2; constructor; auto. Qed.
-Global Instance option_mbind_proper `{Equiv A, Equiv B} :
+Global Instance option_bind_proper `{Equiv A, Equiv B} :
   Proper (((â‰¡) ==> (â‰¡)) ==> (â‰¡@{option A}) ==> (â‰¡@{option B})) mbind.
 Proof. destruct 2; simpl; try constructor; auto. Qed.
-Global Instance option_mjoin_proper `{Equiv A} :
+Global Instance option_join_proper `{Equiv A} :
   Proper ((â‰¡) ==> (â‰¡@{option (option A)})) mjoin.
 Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.