diff --git a/theories/examples/list_rev.v b/theories/examples/list_rev.v index 676c7180dde4563cb74821841f12097a90aa0079..e499654ed6805a5d762ece2ca70063140b5b3125 100644 --- a/theories/examples/list_rev.v +++ b/theories/examples/list_rev.v @@ -62,8 +62,7 @@ Section list_rev_example. iIntros (l xs) "Hl". iDestruct (llist_split with "Hl") as (vs) "[Hl HIT]". iExists l, vs. iFrame "Hl". - iModIntro. - iIntros "Hl". + iModIntro. iIntros "Hl". iSplitL "Hl HIT". { iApply llist_split. rewrite big_sepL2_reverse_2. iExists (reverse vs). iFrame "Hl HIT". }