Commit 6ab9c4e7 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Generate an error message if no `IntoIH` instance exists (instead of just shelving that instance).

parent 3c66abfe
......@@ -2226,9 +2226,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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment