From 7a82a515c12591fa4fab010410b301bcff6b5db1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 8 Aug 2016 11:19:13 +0200
Subject: [PATCH] counter_example: Turn a comment into a proper TODO
---
program_logic/counter_examples.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 540d3fa02..d1fef65e9 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -156,7 +156,7 @@ Module inv. Section inv.
Proof.
iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
iApply (inv_open' i). iSplit; first done.
- (* Can I state a view-shift and immediately run it? *)
+ (* TODO: How can I state a view-shift and immediately run it? *)
iIntros "HaP". iAssert (pvs M0 (finished γ)) with "[HaP]" as "Hf".
{ iDestruct "HaP" as "[Hs | [Hf _]]".
- by iApply start_finish.
--
GitLab