bump gpfsl

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") }
 ]

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κ⌝)

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.