diff --git a/tests/proper.v b/tests/proper.v
index 5efcdbce091f2141489f3ee16a06eeabf75ea862..becefdc8996c66b3d8b7e5524377dda75eb49f97 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 82b1387aedd65b27e5d5fd4020ff8fef91776b8e..179667b663daa6912372b80620143f29d8778ece 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. *)