From 77a0dd03f510de2e4c77abb3434cf87740c09f41 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 3 Oct 2020 11:38:58 +0200
Subject: [PATCH] update dependencies; fix for std++ lemma rename

---
 opam                            | 2 +-
 theories/lifetime/frac_borrow.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/opam b/opam
index 2e92b663..8b3589d5 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 f06e81dd..cb7addfa 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".
-- 
GitLab