From 19d0c303fd32e32922582ac383f8b3dc2c5aa5af Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Sat, 23 Mar 2024 18:31:53 +0100
Subject: [PATCH] Further clean up of proofmode
---
multi_actris/channel/proofmode.v | 11 +++++------
1 file changed, 5 insertions(+), 6 deletions(-)
diff --git a/multi_actris/channel/proofmode.v b/multi_actris/channel/proofmode.v
index a125a6f..f0fff71 100644
--- a/multi_actris/channel/proofmode.v
+++ b/multi_actris/channel/proofmode.v
@@ -397,11 +397,10 @@ Tactic Notation "iProto_consistent_take_step_step" :=
let m2 := fresh in
iIntros (i j m1 m2) "#Hm1 #Hm2";
repeat (destruct i as [|i]=> /=;
- [try (rewrite lookup_total_nil); try (by rewrite iProto_end_message_equivI);
+ [try (by rewrite iProto_end_message_equivI);
iDestruct (iProto_message_equivI with "Hm1")
as "[%Heq1 Hm1']";simplify_eq=> /=|
- try (rewrite lookup_total_nil); try (by rewrite iProto_end_message_equivI)]);
- try (rewrite lookup_total_nil);
+ try (by rewrite iProto_end_message_equivI)]);
try (by rewrite iProto_end_message_equivI);
iDestruct (iProto_message_equivI with "Hm2")
as "[%Heq2 Hm2']";simplify_eq=> /=;
@@ -418,10 +417,10 @@ Tactic Notation "iProto_consistent_take_step_target" :=
iIntros (i j a m); rewrite /valid_target;
iIntros "#Hm1";
repeat (destruct i as [|i]=> /=;
- [try (rewrite lookup_total_nil); try (by rewrite iProto_end_message_equivI);
+ [try (by rewrite iProto_end_message_equivI);
by iDestruct (iProto_message_equivI with "Hm1")
- as "[%Heq1 Hm1']" ; simplify_eq=> /=|
- try (rewrite lookup_total_nil); try (by rewrite iProto_end_message_equivI)]).
+ as "[%Heq1 _]" ; simplify_eq=> /=|
+ try (by rewrite iProto_end_message_equivI)]).
Tactic Notation "iProto_consistent_take_step" :=
try iNext;
--
GitLab