From e2b843075894275afd52c19c83e4f5f812afdbab Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 20 Dec 2016 14:34:51 +0100
Subject: [PATCH] fix an error message in iInduction
---
theories/proofmode/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index fe7df1fec..b580a047a 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -978,7 +978,7 @@ Tactic Notation "iInductionCore" constr(x)
lazymatch goal with
| H : coq_tactics.of_envs _ ⊢ _ |- _ =>
eapply tac_revert_ih;
- [reflexivity || fail "iInduction: persistent context not empty"
+ [reflexivity || fail "iInduction: spatial context not empty"
|apply H|];
clear H; fix_ihs;
let IH' := iFresh' IH in iIntros [IAlwaysElim (IName IH')]
--
GitLab