From d2a0e5d1a29355c95071fe1695e0e4255b2a2803 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 May 2020 16:55:11 +0200
Subject: [PATCH] Name a variable in a `destruct`.

---
 theories/proofmode/coq_tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index cc1805471..7a90a32fd 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.
-- 
GitLab