From 15eef304fee67d203b1c1fdf53b98d44495d12a2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 Sep 2021 11:47:49 +0200
Subject: [PATCH] Fix `iSpecialize` auto framing error message.
This closes issue #432.
---
iris/proofmode/ltac_tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index d9ab16e89..37a802083 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1007,7 +1007,7 @@ Ltac iSpecializePat_go H1 pats :=
[notypeclasses refine (tac_unlock_emp _ _ _)
|notypeclasses refine (tac_unlock_True _ _ _)
|iFrame "∗ #"; notypeclasses refine (tac_unlock _ _ _)
- |fail "iSpecialize: premise cannot be solved by framing"]
+ |fail 1 "iSpecialize: premise cannot be solved by framing"]
|exact eq_refl]; iIntro H1; iSpecializePat_go H1 pats
end.
--
GitLab