From 350f5ecfdb8aadf04632ea7b1b87e4f30dfbbe45 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simonhudon@google.com>
Date: Thu, 13 May 2021 01:22:25 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 iris_heap_lang/derived_laws.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 94c3bcc69..d4a33a568 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -206,7 +206,7 @@ Proof.
 Qed.
 
 Lemma twp_xchg_offset s E l off vs v v' :
-  (vs !! off) = Some v →
+  vs !! off = Some v →
   val_is_unboxed v ->
   [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
 Proof.
-- 
GitLab