Skip to content

GitLab

Commit e2b84307 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix an error message in iInduction

parent 0d471f47
Hide whitespace changes
Inline Side-by-side
theories/proofmode/tactics.v
View file @ e2b84307
...@@ -978,7 +978,7 @@ Tactic Notation "iInductionCore" constr(x) ...@@ -978,7 +978,7 @@ Tactic Notation "iInductionCore" constr(x)
lazymatch goal with lazymatch goal with
| H : coq_tactics.of_envs _ ⊢ _ |- _ => | H : coq_tactics.of_envs _ ⊢ _ |- _ =>
eapply tac_revert_ih; eapply tac_revert_ih;
[reflexivity || fail "iInduction: persistent context not empty" [reflexivity || fail "iInduction: spatial context not empty"
|apply H|]; |apply H|];
clear H; fix_ihs; clear H; fix_ihs;
let IH' := iFresh' IH in iIntros [IAlwaysElim (IName IH')] let IH' := iFresh' IH in iIntros [IAlwaysElim (IName IH')]
......
Markdown is supported
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