diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 95453c55be896474414a38cb310729876f586e66..15a586ab25ea1e02a43c9024600b839fd9f4b3ab 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 :=