Commit 9accfd70 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix issue #198.

parent 7319e95e
Pipeline #9583 passed with stage
in 18 minutes and 59 seconds
...@@ -982,7 +982,7 @@ Tactic Notation "iModIntro" uconstr(sel) := ...@@ -982,7 +982,7 @@ Tactic Notation "iModIntro" uconstr(sel) :=
| MIEnvIsEmpty => fail "iModIntro: persistent context is non-empty" | MIEnvIsEmpty => fail "iModIntro: persistent context is non-empty"
end end
|iSolveTC || |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 lazymatch eval hnf in s with
| MIEnvForall ?C => fail "iModIntro: spatial context does not satisfy" C | MIEnvForall ?C => fail "iModIntro: spatial context does not satisfy" C
| MIEnvIsEmpty => fail "iModIntro: spatial context is non-empty" | MIEnvIsEmpty => fail "iModIntro: spatial context is non-empty"
......
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