From 9accfd708ad534e10b25ca9b9c701cd7259683a2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 Jun 2018 20:50:56 +0200
Subject: [PATCH] Fix issue #198.
---
theories/proofmode/ltac_tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index e48d17176..83a56109c 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -982,7 +982,7 @@ Tactic Notation "iModIntro" uconstr(sel) :=
| MIEnvIsEmpty => fail "iModIntro: persistent context is non-empty"
end
|iSolveTC ||
- let s := lazymatch goal with |- IntoModalPersistentEnv _ _ _ ?s => s end in
+ let s := lazymatch goal with |- IntoModalSpatialEnv _ _ _ ?s _ => s end in
lazymatch eval hnf in s with
| MIEnvForall ?C => fail "iModIntro: spatial context does not satisfy" C
| MIEnvIsEmpty => fail "iModIntro: spatial context is non-empty"
--
GitLab