From 0144c537e880f03275e1b4b9043aeec7960be6c4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Feb 2017 16:06:38 +0100
Subject: [PATCH] Propers for monadic operations on option.

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

diff --git a/theories/option.v b/theories/option.v
index 48b6fba5..ca366407 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -231,9 +231,15 @@ Proof. destruct mx; naive_solver. Qed.
 Lemma bind_with_Some {A} (mx : option A) : mx ≫= Some = mx.
 Proof. by destruct mx. Qed.
 
-Instance option_fmap_proper `{Equiv A, Equiv B} (f : A → B) :
-  Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=option) f).
+Instance option_fmap_proper `{Equiv A, Equiv B} :
+  Proper (((≡) ==> (≡)) ==> (≡) ==> (≡)) (fmap (M:=option) (A:=A) (B:=B)).
 Proof. destruct 2; constructor; auto. Qed.
+Instance option_mbind_proper `{Equiv A, Equiv B} :
+  Proper (((≡) ==> (≡)) ==> (≡) ==> (≡)) (mbind (M:=option) (A:=A) (B:=B)).
+Proof. destruct 2; simpl; try constructor; auto. Qed.
+Instance option_mjoin_proper `{Equiv A} :
+  Proper ((≡) ==> (≡)) (mjoin (M:=option) (A:=A)).
+Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
 
 (** ** Inverses of constructors *)
 (** We can do this in a fancy way using dependent types, but rewrite does
-- 
GitLab