diff --git a/stdpp/base.v b/stdpp/base.v
index f8105fb370340d9d345f7bb22484d130e70b4742..31f4417eaf7311c11a9ca799dda68183e1c0307a 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -1292,7 +1292,7 @@ Global Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 function [f], which is called with the original value. *)
 Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
 Global Hint Mode Alter - - ! : typeclass_instances.
-Global Instance: Params (@alter) 5 := {}.
+Global Instance: Params (@alter) 4 := {}.
 Global Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [partial_alter f k m] should update the value at key [k] using the
diff --git a/tests/proper.v b/tests/proper.v
index 6fecdca0400bfcb58584cc78bc653d28ae5d730d..36249631f6cb23b9d39568f83dbf05f19e6f391e 100644
--- a/tests/proper.v
+++ b/tests/proper.v
@@ -85,6 +85,10 @@ Section map_tests.
   that also allow the function to differ. We test that we can derive simpler
   [Proper]s for a fixed function using both type class inference ([apply _])
   and std++'s [solve_proper] tactic. *)
+  Global Instance map_alter_proper_test (f : A → A) i :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡)) (alter (M:=M A) f i).
+  Proof. apply _. Restart. solve_proper. Abort.
   Global Instance map_zip_proper_test `{Equiv B} :
     Proper ((≡@{M A}) ==> (≡@{M B}) ==> (≡@{M (A * B)})) map_zip.
   Proof. apply _. Restart. solve_proper. Abort.
@@ -103,6 +107,10 @@ Section map_tests.
 End map_tests.
 
 (** And similarly for lists *)
+Global Instance list_alter_proper_test `{!Equiv A} (f : A → A) i :
+  Proper ((≡) ==> (≡)) f →
+  Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
+Proof. apply _. Restart. solve_proper. Abort.
 Global Instance list_fmap_proper_test `{!Equiv A, !Equiv B} (f : A → B) :
   Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap f).
 Proof. apply _. Restart. solve_proper. Abort.