From d83e44a6cb7b550bb40bad6e26a9117881012350 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 May 2020 21:57:16 +0200
Subject: [PATCH] Proper instance with `pointwise_relation` for `from_option`.

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

diff --git a/theories/option.v b/theories/option.v
index f8c284a9..ebbc3679 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -21,7 +21,7 @@ Proof. congruence. Qed.
 (** The [from_option] is the eliminator for option. *)
 Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
   match mx with None => y | Some x => f x end.
-Instance: Params (@from_option) 3 := {}.
+Instance: Params (@from_option) 2 := {}.
 Arguments from_option {_ _} _ _ !_ / : assert.
 
 (** The eliminator with the identity function. *)
@@ -145,8 +145,12 @@ Section setoids.
   Global Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some.
   Proof. inversion_clear 1; split; eauto. Qed.
   Global Instance from_option_proper {B} (R : relation B) (f : A → B) :
-    Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
-  Proof. destruct 3; simpl; auto. Qed.
+    Proper ((≡) ==> R) f →
+    Proper (R ==> (≡) ==> R) (from_option f).
+  Proof. solve_proper. Qed.
+  Global Instance from_option_proper_ext {B} (R : relation B) :
+    Proper (pointwise_relation A R ==> R ==> (=) ==> R) from_option.
+  Proof. solve_proper. Qed.
 End setoids.
 
 Typeclasses Opaque option_equiv.
-- 
GitLab