diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index cc180547136fb42d0114b3294f8c825e666eeb63..7a90a32fdc6e84d74926e238d31c7ff702e27960 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -841,7 +841,7 @@ Lemma tac_löb Δ i Q :
   end →
   envs_entails Δ Q.
 Proof.
-  destruct (envs_app _ _ _) eqn:?; last done.
+  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
   rewrite envs_entails_eq => ?? HQ.
   rewrite (env_spatial_is_nil_intuitionistically Δ) //.
   rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.