From 0387d97bc5d16b1a6ca577e2207a6a34b84e6e79 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Aug 2022 09:39:42 +0200
Subject: [PATCH] Fix `Params` for `alter` and add a test.

---
 stdpp/base.v   | 2 +-
 tests/proper.v | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/stdpp/base.v b/stdpp/base.v
index f8105fb3..31f4417e 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 6fecdca0..36249631 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.
-- 
GitLab