diff --git a/theories/lib/flock.v b/theories/lib/flock.v index 50acead83679970eb8c62f2c0b1310633a7826cd..64b7e1c2b57a0c653f031754c1567eb5a2589c71 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 bf487f53b5d9192f1413310319e4a0030e7054c8..b30255bbac084160a2b49b635b1029ce28988fcb 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.