Fix `Params` of `from_option` to match with !276.

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}.
 

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. *)