From 445154be98d960701cc99bb0105931453ccc327a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 18 Jan 2020 13:15:12 +0100
Subject: [PATCH] bump Iris
---
opam | 2 +-
theories/lifetime/model/definitions.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/opam b/opam
index 4b1891b8..8da289fd 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
- "coq-iris" { (= "dev.2019-12-13.0.335ff6d7") | (= "dev") }
+ "coq-iris" { (= "dev.2020-01-17.1.5088d5b0") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 19961dbf..05cb652b 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -230,7 +230,7 @@ Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) I n :
(∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
lft_vs_inv_go κ f I ≡{n}≡ lft_vs_inv_go κ f' I.
Proof.
- intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ'.
+ intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ' _.
by apply forall_ne=> Hκ.
Qed.
--
GitLab