From 2fcbb0257e20acfba98789731924a033fa84a5d1 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 13 Dec 2016 21:20:20 +0100
Subject: [PATCH] Fix build. Now, this was a compatibility problem....

---
 theories/typing/lft_contexts.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index a1665a3f..a31e1bb0 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -143,7 +143,8 @@ Section lft_contexts.
 
   Lemma incl_local κ κ' κs : (κ, κs) ∈ L → κ' ∈ κs → incl κ κ'.
   Proof.
-    iIntros (? Hκ'κs) "_ H". iDestruct "H" as %(κ0 & EQ). done. simpl in EQ; subst.
+    iIntros (? Hκ'κs) "_ H". iDestruct "H" as %HL.
+    edestruct HL as [κ0 EQ]. done. simpl in EQ; subst.
     iApply lft_le_incl. etrans; last by apply gmultiset_union_subseteq_l.
     clear -Hκ'κs. induction Hκ'κs.
     - apply gmultiset_union_subseteq_l.
-- 
GitLab