From 0c291783639d509056445050de9b21790753f5eb Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Sun, 24 Mar 2024 16:11:31 +0100
Subject: [PATCH] Removed deprecated tactic calls
---
multi_actris/examples/basics.v | 4 ----
1 file changed, 4 deletions(-)
diff --git a/multi_actris/examples/basics.v b/multi_actris/examples/basics.v
index 4656fbd..36c500f 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).
--
GitLab