From 3c4e882edb61530698cb0d0cfc4b9c0597875ad7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 Sep 2021 11:48:15 +0200
Subject: [PATCH] Add tests.

---
 tests/proofmode.ref | 6 ++++++
 tests/proofmode.v   | 8 ++++++++
 2 files changed, 14 insertions(+)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index ce883c7eb..ebb13cbfa 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 03b44f242..e3257f9e5 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.
-- 
GitLab