From ca70af1dbfd36399747867e5acc8d39be85eb1e1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jun 2021 10:52:33 +0200
Subject: [PATCH] Fix `Params` of `from_option` to match with !276.

---
 tests/proper.v    | 7 +++++++
 theories/option.v | 2 +-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/tests/proper.v b/tests/proper.v
index 5efcdbce..becefdc8 100644
--- a/tests/proper.v
+++ b/tests/proper.v
@@ -23,6 +23,13 @@ Section tests.
   Proof. solve_proper. Qed.
 End tests.
 
+Global Instance from_option_proper_test1 `{Equiv A} {B} (R : relation B) (f : A → B) :
+  Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
+Proof. apply _. Qed.
+Global Instance from_option_proper_test2 `{Equiv A} {B} (R : relation B) (f : A → B) :
+  Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
+Proof. solve_proper. Qed.
+
 Section map_tests.
   Context `{FinMap K M} `{Equiv A}.
 
diff --git a/theories/option.v b/theories/option.v
index 82b1387a..179667b6 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.
-Global Instance: Params (@from_option) 3 := {}.
+Global Instance: Params (@from_option) 2 := {}.
 Global Arguments from_option {_ _} _ _ !_ / : assert.
 
 (** The eliminator with the identity function. *)
-- 
GitLab