Bump Iris

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" }
 ]

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)

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