From f5928e3c46219084f1d39ddf640a23dc499d2ccf Mon Sep 17 00:00:00 2001
From: Janggun Lee <leesisi123@naver.com>
Date: Tue, 24 Sep 2024 11:40:27 +0900
Subject: [PATCH] Fix tests
---
tests/proofmode_iris.ref | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 352669721..f55643d50 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -269,7 +269,7 @@ Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]".
--------------------------------------□
WP e {{ _, ∃ n : nat, Φ n }}
"iInv_WP"
- : string
+ : string
2 goals
hlc : has_lc
@@ -289,7 +289,7 @@ goal 2 is:
--------------------------------------∗
WP e @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
"iMod_TWP_mask_mismatch"
- : string
+ : string
The command has indeed failed with message:
Tactic failure:
"Goal and eliminated modality must have the same mask.
@@ -299,7 +299,7 @@ Tactic failure:
"Goal and eliminated modality must have the same mask.
Use [iApply fupd_twp; iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]".
"iMod_TWP_atomic_mask_mismatch"
- : string
+ : string
The command has indeed failed with message:
Tactic failure:
"Goal and eliminated modality must have the same mask.
@@ -309,7 +309,7 @@ Tactic failure:
"Goal and eliminated modality must have the same mask.
Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]".
"iFrame_TWP_no_instantiate"
- : string
+ : string
1 goal
hlc : has_lc
@@ -323,7 +323,7 @@ Tactic failure:
--------------------------------------□
WP e [{ _, ∃ n : nat, Φ n }]
"iInv_TWP"
- : string
+ : string
2 goals
hlc : has_lc
--
GitLab