diff --git a/opam.pins b/opam.pins
index c16dcc84e54cbcad9dec0dc93d6a58472aca5fd6..d9fa24e4f5d8ae66507830c27669d190ae3e70ed 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp ee6200b4d74bfd06034f3cc36d1afdc309427e5c
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 24cc2e4786b2344e092e412f56e96c6971ab60d8
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index c410171fe0bd0d7f38b48f0f5acfaf7b25223a71..c49bfa2402699edf4c83a1515c8e0e4050e1f230 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -279,7 +279,8 @@ Proof.
   split; try apply _.
   - intros n [[[a|]|] b]; rewrite !auth_validN_eq; try
       naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN.
-  - intros [??]. apply Some_proper. by f_equiv; rewrite /= cmra_morphism_core.
+  - intros [??]. apply Some_proper; rewrite /auth_map /=.
+    by f_equiv; rewrite /= cmra_morphism_core.
   - intros [[?|]?] [[?|]?]; try apply Auth_proper=>//=; by rewrite cmra_morphism_op.
 Qed.
 Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1796ace9ef67df7454543799ac464d0fdd48c32b..ce44a5526a985b69332496fb1c3819353607192d 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -239,17 +239,18 @@ End contractive.
 
 Ltac f_contractive :=
   match goal with
-  | |- ?f _ ≡{_}≡ ?f _ => apply (_ : Proper (dist_later _ ==> _) f)
-  | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (dist_later _ ==> _ ==> _) f)
-  | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f)
+  | |- ?f _ ≡{_}≡ ?f _ => simple apply (_ : Proper (dist_later _ ==> _) f)
+  | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (dist_later _ ==> _ ==> _) f)
+  | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (_ ==> dist_later _ ==> _) f)
   end;
   try match goal with
   | |- @dist_later ?A _ ?n ?x ?y =>
          destruct n as [|n]; [exact I|change (@dist A _ n x y)]
   end;
-  try reflexivity.
+  try simple apply reflexivity.
 
-Ltac solve_contractive := solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]).
+Ltac solve_contractive :=
+  solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]).
 
 (** Limit preserving predicates *)
 Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop :=