From 39e504e3f4f9bec27edc3899cbff06338c9b16c4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 12 May 2020 14:51:53 +0200
Subject: [PATCH] =?UTF-8?q?Tweak=20error=20message=20and=20test=20case=20o?=
 =?UTF-8?q?f=20`iL=C3=B6b`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 tests/proofmode.ref               | 4 ++--
 tests/proofmode.v                 | 4 ++--
 theories/proofmode/ltac_tactics.v | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 3275844a0..34d52265b 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -621,10 +621,10 @@ k is used in hypothesis Hk.
      : string
 The command has indeed failed with message:
 Tactic failure: iRevert: k is used in hypothesis "Hk".
-"iLöb_no_bi"
+"iLöb_no_BiLöb"
      : string
 The command has indeed failed with message:
-Tactic failure: iLöb: Löb induction not supported for this BI.
+Tactic failure: iLöb: no 'BiLöb' instance found.
 "test_pure_name"
      : string
 1 subgoal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9670b934a..2df448f52 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1127,8 +1127,8 @@ Section error_tests_bi.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 
-Check "iLöb_no_bi".
-Lemma iLöb_no_bi P : ⊢ P.
+Check "iLöb_no_BiLöb".
+Lemma iLöb_no_BiLöb P : ⊢ P.
 Proof. Fail iLöb as "IH". Abort.
 End error_tests_bi.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 2604bdd67..95810df70 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -2534,7 +2534,7 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
      refine should use the other unification algorithm, which should
      not have this issue. *)
   notypeclasses refine (tac_löb _ IH _ _ _ _);
-    [iSolveTC || fail "iLöb: Löb induction not supported for this BI"
+    [iSolveTC || fail "iLöb: no 'BiLöb' instance found"
     |reflexivity || fail "iLöb: spatial context not empty, this should not happen"
     |pm_reduce;
      lazymatch goal with
-- 
GitLab