diff --git a/multi_actris/examples/basics.v b/multi_actris/examples/basics.v index 4656fbd84a91c5f2fa9526cc8ad05c6efbc262c6..36c500f5638399b41d1f224f642729436330879d 100644 --- a/multi_actris/examples/basics.v +++ b/multi_actris/examples/basics.v @@ -492,13 +492,11 @@ Section forwarder_rec. - iExists _. iSplit; [done|]. iSplit; [done|]. iProto_consistent_take_step. iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|]. - repeat clean_map 1. repeat clean_map 2. repeat clean_map 0. iNext. iEval (rewrite iProto_forwarder_rec_1_unfold). iEval (rewrite iProto_forwarder_rec_n_unfold). iProto_consistent_take_step. iIntros "_". iSplit; [done|]. iSplit; [done|]. - repeat clean_map 1. repeat clean_map 2. repeat clean_map 0. iEval (rewrite -iProto_forwarder_rec_1_unfold). iEval (rewrite -iProto_forwarder_rec_n_unfold). iEval (rewrite -iProto_forwarder_rec_n_unfold). @@ -506,13 +504,11 @@ Section forwarder_rec. - iExists _. iSplit; [done|]. iSplit; [done|]. iProto_consistent_take_step. iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|]. - repeat clean_map 1. repeat clean_map 2. repeat clean_map 0. iNext. iEval (rewrite iProto_forwarder_rec_1_unfold). iEval (rewrite iProto_forwarder_rec_n_unfold). iProto_consistent_take_step. iIntros "_". iSplit; [done|]. iSplit; [done|]. - repeat clean_map 1. repeat clean_map 3. repeat clean_map 0. iEval (rewrite -iProto_forwarder_rec_1_unfold). iEval (rewrite -iProto_forwarder_rec_n_unfold). iEval (rewrite -iProto_forwarder_rec_n_unfold).