From 82563700bd5619ade9ea14d7c3965df2178658e5 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Fri, 16 Nov 2018 22:17:48 +0100 Subject: [PATCH] a wee cleanup --- theories/lib/flock.v | 2 +- theories/tests/unknowns.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/lib/flock.v b/theories/lib/flock.v index 50acead..64b7e1c 100644 --- a/theories/lib/flock.v +++ b/theories/lib/flock.v @@ -656,7 +656,7 @@ Section flock. iDestruct (own_valid_2 with "Haprops HI") as %[Hfoo _]%auth_valid_discrete_2. - (* TODO: RK, please take a look at this horrific script *) + (* TODO: RK, can this proof script be simplified? The idea is not complicated. *) (* We are going to separate the active resources I out of the fp map *) pose (I'' := fmap res_name I). assert (∃ P', P' ##ₘ I'' ∧ fp ≡ P' ∪ I'') as [P' HP']. diff --git a/theories/tests/unknowns.v b/theories/tests/unknowns.v index bf487f5..b30255b 100644 --- a/theories/tests/unknowns.v +++ b/theories/tests/unknowns.v @@ -36,7 +36,7 @@ Section tests_vcg. intros. vcg. iExists (n). repeat iSplit; eauto. { iPureIntro. lia. } iIntros (l) "? Hl". assert (∃ m, n = S m) as [k ->]. exists (pred n). lia. - iDestruct "Hl" as "[Hl Hls]". (* TODO: this looks ridiculous *) + iDestruct "Hl" as "[Hl Hls]". vcg_continue. eauto 42 with iFrame. Qed. -- 2.24.1