diff --git a/tests/proofmode.ref b/tests/proofmode.ref index ce883c7eb98eb7a49acf25b11f63a43eaedf61d8..ebb13cbfacdb8717ae2d2c4570b18a17487ca9c4 100644 --- a/tests/proofmode.ref +++ b/tests/proofmode.ref @@ -589,6 +589,12 @@ Tactic failure: iSpecialize: "H" not found. : string The command has indeed failed with message: Tactic failure: iSpecialize: "H" not found. +"iSpecialize_autoframe_fail" + : string +The command has indeed failed with message: +Tactic failure: iSpecialize: premise cannot be solved by framing. +The command has indeed failed with message: +Tactic failure: iSpecialize: premise cannot be solved by framing. "iExact_fail" : string The command has indeed failed with message: diff --git a/tests/proofmode.v b/tests/proofmode.v index 03b44f242cce64a05a09000da3b14566dd5e92b6..e3257f9e574a38bf1932ccb0c05d02c0f70ebfeb 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -1305,6 +1305,14 @@ Proof. iIntros "HW HP". Fail iSpecialize ("HW" with "H"). Abort. +Check "iSpecialize_autoframe_fail". +Lemma iSpecialize_autoframe_fail P Q : (P -∗ Q) -∗ Q. +Proof. + iIntros "H". + Fail iSpecialize ("H" with "[$]"). + Fail iApply ("H" with "[$]"). +Abort. + Check "iExact_fail". Lemma iExact_fail P Q : <affine> P -∗ Q -∗ <affine> P.