Bump std++ (filter_insert).

coq-iris.opam

@@ -15,7 +15,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
 
 depends: [
   "coq" { (>= "8.12" & < "8.15~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2021-07-27.2.7d34364f") | (= "dev") }
+  "coq-stdpp" { (= "dev.2021-07-28.2.c4a352b1") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]

iris/algebra/big_op.v

@@ -411,7 +411,7 @@ Section gmap.
     induction m as [|k v m ? IH] using map_ind.
     { by rewrite map_filter_empty !big_opM_empty. }
     destruct (decide (φ (k, v))).
-    - rewrite map_filter_insert //.
+    - rewrite map_filter_insert_True //.
       assert (filter φ m !! k = None) by (apply map_filter_lookup_None; eauto).
       by rewrite !big_opM_insert // decide_True // IH.
     - rewrite map_filter_insert_not' //; last by congruence.