From 797c363b285fec603b4fb7a15fdf4729e515f4d9 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Thu, 20 May 2021 18:12:30 +0200
Subject: [PATCH] Bump Iris
---
opam | 2 +-
theories/prelude/ctx_subst.v | 2 ++
theories/typing/types.v | 2 +-
3 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/opam b/opam
index 5413fd9..7472333 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-heap-lang" { (= "dev.2021-04-22.1.35e8d8d7") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2021-05-20.3.96191ed7") | (= "dev") }
"coq-autosubst" { = "dev" }
]
diff --git a/theories/prelude/ctx_subst.v b/theories/prelude/ctx_subst.v
index 1668ce0..e699cd4 100644
--- a/theories/prelude/ctx_subst.v
+++ b/theories/prelude/ctx_subst.v
@@ -25,6 +25,8 @@ Fixpoint subst_map_ctx_item (es : stringmap val) (K : ectx_item)
| LoadCtx => LoadCtx
| StoreLCtx v2 => StoreLCtx v2
| StoreRCtx e1 => StoreRCtx (subst_map es e1)
+ | XchgLCtx v2 => XchgLCtx v2
+ | XchgRCtx e1 => XchgRCtx (subst_map es e1)
| CmpXchgLCtx v1 v2 => CmpXchgLCtx v1 v2
| CmpXchgMCtx e0 v2 => CmpXchgMCtx (subst_map es e0) v2
| CmpXchgRCtx e0 e1 => CmpXchgRCtx (subst_map es e0) (subst_map es e1)
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 00d84e0..664498d 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -272,7 +272,7 @@ Local Fixpoint is_closed_expr_set (X : stringset) (e : expr) : bool :=
| Rec f x e => is_closed_expr_set (maybe_insert_binder f (maybe_insert_binder x X)) e
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Free e | Load e =>
is_closed_expr_set X e
- | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 =>
+ | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 | Xchg e1 e2 =>
is_closed_expr_set X e1 && is_closed_expr_set X e2
| If e0 e1 e2 | Case e0 e1 e2 | CmpXchg e0 e1 e2 | Resolve e0 e1 e2 =>
is_closed_expr_set X e0 && is_closed_expr_set X e1 && is_closed_expr_set X e2
--
GitLab