From 45b4a2d2801b86189aa7be4ccb43c4af285ecb2e Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@bedrocksystems.com>
Date: Thu, 21 Mar 2024 22:30:15 +0100
Subject: [PATCH] iFrame: Do not call `cbv` on user terms in contexts
---
iris/proofmode/ltac_tactics.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 95453c55b..15a586ab2 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -418,7 +418,7 @@ Ltac iFrameAnyIntuitionistic :=
match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
match goal with
| |- envs_entails ?Δ _ =>
- let Hs := eval cbv in (env_dom (env_intuitionistic Δ)) in go Hs
+ let Hs := eval lazy in (env_dom (env_intuitionistic Δ)) in go Hs
end.
Ltac iFrameAnySpatial :=
@@ -427,7 +427,7 @@ Ltac iFrameAnySpatial :=
match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
match goal with
| |- envs_entails ?Δ _ =>
- let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
+ let Hs := eval lazy in (env_dom (env_spatial Δ)) in go Hs
end.
Local Ltac _iFrame_go Hs :=
--
GitLab