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

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

diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 031de179b..fa98c6762 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -385,7 +385,7 @@ Proof.
   rewrite -wp_bind. eapply wand_apply; first by eapply wp_xchg.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id.
-    by apply later_mono, sep_mono_r, wand_mono.
+  by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 Lemma tac_twp_xchg Δ s E i K l v v' Φ :
   envs_lookup i Δ = Some (false, l ↦ v)%I →
-- 
GitLab