diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref index 35266972179845b2679ae2c5de80b2488a1c72d6..f55643d50f6dde9b8a87cdf3668e2822f6b78b3e 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