From 223cd6a5724ffd1bfb4d20bc1243cae3cc2c64a8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 3 Sep 2021 12:40:40 +0200
Subject: [PATCH] Generate an error message if no `IntoIH` instance exists
(instead of just shelving that instance).
---
iris/proofmode/ltac_tactics.v | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 8bed13969..118e5b711 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -2312,9 +2312,12 @@ Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
let rec fix_ihs rev_tac :=
lazymatch goal with
| H : context [envs_entails _ _] |- _ =>
- eapply (tac_revert_ih _ _ _ H _);
- [pm_reflexivity
- || fail "iInduction: spatial context not empty, this should not happen"
+ notypeclasses refine (tac_revert_ih _ _ _ H _ _ _);
+ [iSolveTC ||
+ let φ := match goal with |- IntoIH ?φ _ _ => φ end in
+ fail "iInduction: cannot import IH" φ "into proof mode context"
+ |pm_reflexivity ||
+ fail "iInduction: spatial context not empty, this should not happen"
|clear H];
fix_ihs ltac:(fun j =>
let IH' := eval vm_compute in
--
GitLab