diff --git a/opam b/opam
index 875c0e1477675ae39aad1e7f9fbfa27fa172438b..b7703746b2e8d9f142e97b80f2344e11d9eff995 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 02dc8eee40f6c82f6a6260f2c02379d280f007e9..da79942eb7a5c7da6653a3217b5972229dac5f37 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 82d427ac4740c40094859c0f83df7d5ae1f2a0cc..9841715da623805860363b9a19027196280dfa53 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.