From c9ee4e7c69893f38a029614c6893e0cd03a53333 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 9 Jun 2021 01:35:33 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20`option=5Fmbind=5Fproper`=20=E2=86=92?=
 =?UTF-8?q?=20`option=5Fbind=5Fproper`=20and=20`option=5Fmjoin=5Fproper`?=
 =?UTF-8?q?=20=E2=86=92=20`option=5Fjoin=5Fproper`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/option.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/option.v b/theories/option.v
index 412cd5ce..28ecff3b 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.
 
-- 
GitLab