diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 95453c55be896474414a38cb310729876f586e66..4db325d7c1e775d6bde4b45d891b189d15ccff57 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -418,7 +418,8 @@ 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
+     (* [lazy] because [Δ] involves user terms *)
+     let Hs := eval lazy in (env_dom (env_intuitionistic Δ)) in go Hs
   end.
 
 Ltac iFrameAnySpatial :=
@@ -427,7 +428,8 @@ 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
+     (* [lazy] because [Δ] involves user terms *)
+     let Hs := eval lazy in (env_dom (env_spatial Δ)) in go Hs
   end.
 
 Local Ltac _iFrame_go Hs :=
@@ -1021,7 +1023,8 @@ Tactic Notation "iSpecializeCore" open_constr(H)
        (* Check if we should use [tac_specialize_intuitionistic_helper]. Notice
        that [pm_eval] does not unfold [use_tac_specialize_intuitionistic_helper],
        so we should do that first. *)
-       let b := eval cbv [use_tac_specialize_intuitionistic_helper] in
+       (* [lazy] because [Δ] involves user terms *)
+       let b := eval lazy [use_tac_specialize_intuitionistic_helper] in
          (if p then use_tac_specialize_intuitionistic_helper Δ pat else false) in
        lazymatch eval pm_eval in b with
        | true =>
@@ -1030,7 +1033,8 @@ Tactic Notation "iSpecializeCore" open_constr(H)
           lazymatch iTypeOf H with
           | Some (?q, _) =>
              let PROP := iBiOfGoal in
-             lazymatch eval compute in (q || tc_to_bool (BiAffine PROP)) with
+             (* [lazy] because [PROP] involves user terms *)
+             lazymatch eval lazy in (q || tc_to_bool (BiAffine PROP)) with
              | true =>
                 notypeclasses refine (tac_specialize_intuitionistic_helper _ H _ _ _ _ _ _ _ _ _ _);
                   [pm_reflexivity
@@ -1684,7 +1688,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=
      (** This case is used to make the tactic work in [Z_scope]. It would be
      better if we could bind tactic notation arguments to notation scopes, but
      that is not supported by Ltac. *)
-     let n := eval compute in (Z.to_nat lem) in intro_destruct n
+     let n := eval cbv in (Z.to_nat lem) in intro_destruct n
   | ident => tac lem
   | string => tac constr:(INamed lem)
   | _ => iPoseProofCore lem as p tac
diff --git a/iris/proofmode/reduction.v b/iris/proofmode/reduction.v
index ff036d248d5ef899886c9e5041a9a1ffa2815475..be61cf47d2e25c0d2904b6de26f3057606024792 100644
--- a/iris/proofmode/reduction.v
+++ b/iris/proofmode/reduction.v
@@ -2,11 +2,41 @@ From iris.bi Require Import bi telescopes.
 From iris.proofmode Require Import base environments.
 From iris.prelude Require Import options.
 
-(** Called by all tactics to perform computation to lookup items in the
-    context.  We avoid reducing anything user-visible here to make sure we
-    do not reduce e.g. before unification happens in [iApply].
-    This needs to contain all definitions used in the user-visible statements in
-    [coq_tactics], and their dependencies. *)
+(** The following tactics should be used when performing computation in the
+proofmode:
+
+- Use [cbv]/[vm_compute] (depending on expected size of computation) if the
+  expected result is a simple term (say, a boolean, number, list of strings),
+  and the input term does *not* involve user terms (such as bodies of hypotheses
+  in the proof mode environment).
+- Use [lazy] if the expected result is a simple term and the input term *does*
+  involve user terms.
+- Use [pm_eval] otherwise, particularly to compute new proof mode environments
+  and to lookup items in the proof mode environment.
+
+The reduction [pm_eval] avoids reducing anything user-visible to make sure
+we do not reduce e.g., before unification happens in [iApply]. This needs to
+contain all definitions used in the user-visible statements in [coq_tactics],
+and their dependencies.
+
+Examples:
+
+- [envs_lookup i Δ], where [Δ] is a proof mode environment. This should be
+  computed using [pm_eval] because [Δ] involves user terms and the result is
+  also a user term (a hypothesis).
+- [dom Δ], where [Δ] is a proof mode environment. This should be computed with
+  [lazy] because [Δ] involves user terms and the result is a list of strings.
+  This should *never* be computed using [cbv]/[vm_compute] as that would eagerly
+  unfold all hypotheses in [Δ]. Note that in this specific case one could also
+  use [pm_eval] because all definitions in [dom] are whitelisted by [pm_eval].
+  However, [lazy] is more useful when considering [f (dom Δ)] where [f] is not
+  whitelisted, as [pm_eval] would simply get stuck.
+- [tc_to_bool (BiAffine PROP)]. This should be computed using [lazy] as [PROP]
+  involves user terms (a BI canonical structure instance) and the result is a
+  mere Boolean. This term trivially normalizes with [lazy] to a Boolean (which
+  is present as implicit parameter derived by TC search), while [cbv] would
+  eagerly normalize the whole of [PROP] (i.e., all BI operations contained in
+  the record). *)
 Declare Reduction pm_eval := cbv [
   (* base *)
   base.negb base.beq