diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index cb2349e671d261a1473accee2843b132ff1e875e..3e3d103fe2bee3905a6d0cd15a5969abee05b876 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -33,8 +33,8 @@ Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
   env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
 }.
 
-Instance envs_dom {M} : Dom (envs M) stringset := λ Δ,
-  dom stringset (env_persistent Δ) ∪ dom stringset (env_spatial Δ).
+Definition envs_dom {M} (Δ : envs M) : list string :=
+  env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
 
 Definition envs_lookup {M} (i : string) (Δ : envs M) : option (bool * uPred M) :=
   let (Γp,Γs) := Δ in
diff --git a/proofmode/environments.v b/proofmode/environments.v
index aa5cc9131755d50f531fcd9bca5ad95e15b1875b..0278dba89e3f6880e4cdfba5199e1722ef78a2b3 100644
--- a/proofmode/environments.v
+++ b/proofmode/environments.v
@@ -32,11 +32,8 @@ Fixpoint env_to_list {A} (E : env A) : list A :=
 Coercion env_to_list : env >-> list.
 Instance: Params (@env_to_list) 1.
 
-Instance env_dom {A} : Dom (env A) stringset :=
-  fix go Γ := let _ : Dom _ _ := @go in
-  match Γ with Enil => ∅ | Esnoc Γ i _ => {[ i ]} ∪ dom stringset Γ end.
-Fixpoint env_dom_list {A} (Γ : env A) : list string :=
-  match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom_list Γ end.
+Fixpoint env_dom {A} (Γ : env A) : list string :=
+  match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
 
 Fixpoint env_fold {A B} (f : B → A → A) (x : A) (Γ : env B) : A :=
   match Γ with
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index c3491ace52686a8dc1ceaf20cd404c242216c0f2..ce0289e4a9c104ebdef438ccfe570727712e2036 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -22,13 +22,10 @@ Ltac env_cbv :=
 Ltac iFresh :=
   lazymatch goal with
   |- of_envs ?Δ ⊢ _ =>
-      match goal with
-      | _ => eval vm_compute in (fresh_string_of_set "~" (dom stringset Δ))
-      | _ =>
-         (* [vm_compute fails] if [Δ] contains evars, so fall-back to [cbv] *)
-         let Hs := eval cbv in (dom stringset Δ) in
-         eval vm_compute in (fresh_string_of_set "~" Hs)
-      end
+     (* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
+     first use [cbv] to compute the domain of [Δ] *)
+     let Hs := eval cbv in (envs_dom Δ) in
+     eval vm_compute in (fresh_string_of_set "~" (of_list Hs))
   | _ => constr:"~"
   end.
 
@@ -383,8 +380,7 @@ Tactic Notation "iFrame" :=
     | ?H :: ?Hs => try iFrame H; go Hs
     end in
   match goal with
-  | |- of_envs ?Δ ⊢ _ =>
-        let Hs := eval cbv in (env_dom_list (env_spatial Δ)) in go Hs
+  | |- of_envs ?Δ ⊢ _ => let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
   end.
 
 Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
@@ -681,7 +677,7 @@ idents I do not know how to do this better. *)
 Local Ltac iLöbHelp IH tac_before tac_after :=
   match goal with
   | |- of_envs ?Δ ⊢ _ =>
-     let Hs := constr:(reverse (env_dom_list (env_spatial Δ))) in
+     let Hs := constr:(reverse (env_dom (env_spatial Δ))) in
      iRevert ["★"]; tac_before;
      eapply tac_löb with _ IH;
        [reflexivity