From 151d4e462a31067a770b870461d5dc49bb30cfe8 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 9 Oct 2019 12:03:06 +0200
Subject: [PATCH] bump iris
---
opam | 2 +-
theories/lang/expr_semantics.v | 4 ++--
theories/lang/helpers.v | 4 ++--
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/opam b/opam
index 153c805..1869a25 100644
--- a/opam
+++ b/opam
@@ -7,7 +7,7 @@ synopsis: "The Coq artifact for 'Stacked Borrows'"
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
- "coq-iris" { (= "dev.2019-08-29.2.b75bb397") | (= "dev") }
+ "coq-iris" { (= "dev.2019-09-19.3.aa7871c7") | (= "dev") }
"coq-paco" { (= "3.0.0") }
"coq-equations" { (= "1.2~beta+8.8") | (= "1.2~beta+8.9") }
]
diff --git a/theories/lang/expr_semantics.v b/theories/lang/expr_semantics.v
index 88f8344..8053391 100644
--- a/theories/lang/expr_semantics.v
+++ b/theories/lang/expr_semantics.v
@@ -249,13 +249,13 @@ Equations read_mem (l: loc) (n: nat) h: option value :=
Definition fresh_block (h : mem) : block :=
let loclst : list loc := elements (dom (gset loc) h) in
- let blockset : gset block := foldr (λ l, ({[l.1]} ∪)) ∅ loclst in
+ let blockset : gset block := foldr (λ l, ({[l.1]} ∪.)) ∅ loclst in
fresh blockset.
Lemma is_fresh_block h i : (fresh_block h,i) ∉ dom (gset loc) h.
Proof.
assert (∀ l (ls: list loc) (X : gset block),
- l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪)) X ls) as help.
+ l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪.)) X ls) as help.
{ induction 1; set_solver. }
rewrite /fresh_block /shift /= -elem_of_elements.
move=> /(help _ _ ∅) /=. apply is_fresh.
diff --git a/theories/lang/helpers.v b/theories/lang/helpers.v
index d1d596f..59f108b 100644
--- a/theories/lang/helpers.v
+++ b/theories/lang/helpers.v
@@ -102,11 +102,11 @@ Instance nat_sqsubseteq : SqSubsetEq nat := le.
Instance nat_sqsubseteq_po : @PartialOrder nat (⊑) := _.
Instance elem_of_list_suffix_proper {A : Type} (x:A) :
- Proper ((suffix) ==> impl) (x ∈).
+ Proper ((suffix) ==> impl) (x ∈.).
Proof. intros l1 l2 [? ->] ?. rewrite elem_of_app. by right. Qed.
Instance elem_of_list_sublist_proper {A : Type} (x:A) :
- Proper ((sublist) ==> impl) (x ∈).
+ Proper ((sublist) ==> impl) (x ∈.).
Proof.
intros l1 l2 SUB. induction SUB; [done|..].
- rewrite 2!elem_of_cons. intros []; [by left|right; auto].
--
GitLab