diff --git a/opam b/opam
index aad382cfae8dd95126d9c1b22bbdfaa9a4b83b4c..4f214a0e708c727e5378a40bf3a67334c5b4e2d6 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
 depends: [
-  "coq-iris" { (= "dev.2020-09-03.1.7dd1b9af") | (= "dev") }
+  "coq-iris" { (= "dev.2020-09-15.3.986a8883") | (= "dev") }
 ]
diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
index 7bf226091e656d8bb81e90f2eceb66c7ef1cac3c..1bf752315342ee3a4d3cbd3e9eb02faa7bd66324 100755
--- a/theories/logrel/examples/double.v
+++ b/theories/logrel/examples/double.v
@@ -113,10 +113,10 @@ Section double.
     - iIntros (v1 v2) "[[[H1 Hγ]|H1] [[H2 Hγ']|H2]] !>".
       + by iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
       + iDestruct "H2" as (v2') "(_&H1'&HP)".
-        iDestruct (own_valid_2 with "H1 H1'") as %[_ [=->]%agree_op_invL'].
+        iDestruct (own_valid_2 with "H1 H1'") as %[_ [=->]%to_agree_op_inv_L].
         iApply "HΦ"; auto.
       + iDestruct "H1" as (v1') "(_&H2'&HP)".
-        iDestruct (own_valid_2 with "H2 H2'") as %[_ [=->]%agree_op_invL'].
+        iDestruct (own_valid_2 with "H2 H2'") as %[_ [=->]%to_agree_op_inv_L].
         iApply "HΦ"; auto.
       + iDestruct "H1" as (v1') "[H1 _]"; iDestruct "H2" as (v2') "(_&H2&_)".
         by iDestruct (own_valid_2 with "H1 H2") as %[].