From c7cae6a1163ab9899aa61819ad5cbb45fe40c209 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Sun, 19 Jan 2020 10:29:28 +0100
Subject: [PATCH] bump gpfsl

---
 opam                                  | 2 +-
 theories/lifetime/model/accessors.v   | 2 +-
 theories/lifetime/model/definitions.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/opam b/opam
index 875c0e14..b7703746 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2019-12-16.1.573302f9") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-01-18.1.38a1445a") | (= "dev") }
 ]
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 02dc8eee..da79942e 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -64,7 +64,7 @@ Lemma extend_lft_view A κ q V :
   ∃ A', (q).[κ] V ∗ own_alft_auth A' ∗ ⌜atomic_map_extension A A' κ V⌝.
 Proof.
   iIntros "Htok HA". rewrite /lft_tok /= . setoid_rewrite ->monPred_at_big_sepMS.
-  iDestruct (big_opMS_forall (A := atomic_lft)
+  iDestruct (big_opMS_gen_proper (A := atomic_lft)
     (λ P Q, ∀ A, P -∗ own_alft_auth A ==∗
          ∃ A', own_alft_auth A' ∗ Q ∗ ⌜∀ Λ, fst <$> A' !! Λ = fst <$> A !! Λ⌝ ∗
                     ⌜∀ κ Vκ, lft_has_view A κ Vκ → lft_has_view A' κ Vκ⌝)
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 82d427ac..9841715d 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -248,7 +248,7 @@ Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → monPred) Vs I n :
   (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
   lft_vs_inv_go κ f Vs I ≡{n}≡ lft_vs_inv_go κ f' Vs I.
 Proof.
-  intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ'.
+  intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ' ?.
   apply forall_ne=> Hκ. by rewrite Hf.
 Qed.
 
-- 
GitLab