From 42e0d03d239acd38f03351fda422c491b2bf495e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 5 Apr 2020 09:35:06 +0200
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/experimental/helping/helping_stack.v | 2 +-
theories/logic/spec_ra.v | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/opam b/opam
index 7af1e70..99972c6 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
- "coq-iris" { (= "dev.2020-04-02.5.fa438702") | (= "dev") }
+ "coq-iris" { (= "dev.2020-04-04.3.9b2ad256") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index cb1877a..8bbf9cb 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -124,7 +124,7 @@ Section refinement.
rewrite auth_auth_valid. done. }
iPureIntro.
revert Hfoo.
- rewrite singleton_included=> -[av []].
+ rewrite singleton_included_l=> -[av []].
revert Hvalid.
rewrite /to_offer_reg !lookup_fmap.
case: (N !! o)=> [av'|] Hvalid; last by inversion 1.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index e5cff14..ef586ca 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -113,7 +113,7 @@ Section conversions.
Lemma tpool_singleton_included tp j e :
{[j := Excl e]} ≼ to_tpool tp → tp !! j = Some e.
Proof.
- move=> /singleton_included [ex [/leibniz_equiv_iff]].
+ move=> /singleton_included_l [ex [/leibniz_equiv_iff]].
rewrite tpool_lookup fmap_Some=> [[e' [-> ->]] /Excl_included ?]. by f_equal.
Qed.
Lemma tpool_singleton_included' tp j e :
--
GitLab