diff --git a/opam b/opam
index 5413fd9741d4fdfd182a926a013a1d3558c36e9e..747233393d7eb49831b17375ce9e126b6497931c 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 1668ce07458af5b4457e51acb712afe480421650..e699cd4bde7cb9f7e5dba3858daed119bb23ba61 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 00d84e04c0ddbc838f874387abc7c403fd7bf8b0..664498d0319a1b900e01271cbc18974dd3f6b8e4 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