diff --git a/opam b/opam
index 2e92b663e868f142306005556fd66e7a9b5542ee..8b3589d501569573d03632415effcee2fdbb6cb9 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-10-01.3.8f6c063a") | (= "dev") }
+  "coq-iris" { (= "dev.2020-10-02.0.5ab2529d") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index f06e81dd23542c006f8d192bebe2a39fe41128cb..cb7addfa1e4ec5be9920e26f7d35f9c5c4e37db8 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -76,7 +76,7 @@ Section frac_bor.
     iIntros "#Hφ (H & Hown & Hφ1)". iNext.
     iDestruct "H" as (qφ) "(Hφqφ & Hown' & [%|Hq])".
     { subst. iCombine "Hown'" "Hown" as "Hown".
-      by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
+      by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_ge. }
     rewrite /frac_bor_inv. iApply bi.sep_exist_r. iExists (q + qφ)%Qp.
     iDestruct "Hq" as (q' Hqφq') "Hq'κ". iCombine "Hown'" "Hown" as "Hown".
     iDestruct (own_valid with "Hown") as %Hval. rewrite comm_L. iFrame "Hown".