From 353e29002389508959c2f4370737c67b3d1c0241 Mon Sep 17 00:00:00 2001
From: Gaurav Parthasarathy <gauravp@student.ethz.ch>
Date: Mon, 8 Jul 2019 11:56:49 +0200
Subject: [PATCH] minor change
---
theories/logatom/rdcss/rdcss.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 4aa10662..27a30a51 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -387,7 +387,8 @@ Section rdcss.
(* FIXME: proof duplication *)
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
iIntros (vs'' ->) "Hp". iModIntro.
- iSplitL "Done Hp". { by eauto 12 with iFrame. } iModIntro.
+ iSplitL "Done Hp". { by eauto 12 with iFrame. }
+ iModIntro.
iSplitL "Hln Hrest". { by eauto 12 with iFrame. }
wp_seq. iApply "HQ".
iApply state_done_extract_Q; done.
--
GitLab