From cb908b612fe6601f498bde9e81f8bc42e4ae0f10 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 9 Dec 2016 23:18:56 +0100
Subject: [PATCH] fix build

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

diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 984f3d09..4aa81f91 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -25,7 +25,7 @@ Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
     as %[[? [Hl ?]]%singleton_included _]%auth_valid_discrete_2.
   unfold to_ilftUR in *. simplify_map_eq.
-  destruct (fmap_Some_equiv' _ _ _ Hl) as (?&?&?). eauto.
+  destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.
 
 Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
-- 
GitLab