diff --git a/opam b/opam
index 2a2cd4bd85c64138d16294cce00bd6aa1c925428..4005adae8070cfc2dfa97933ec6aeb477f79a011 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-04-25.0.8e1ed3d2") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-05-02.0.92f26ecd") | (= "dev") }
 ]
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index ba09a27b6c22b8115cc3987f7576529638e209d2..e6e09aa41232ce6fdb36fc48ed75d4c8fdd08540 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -218,7 +218,7 @@ Proof.
   iAssert ([∗ map] γ↦_ ∈ f, ▷ Φ γ V)%I with "[HP]" as "HP'".
   { rewrite -big_sepM_later -monPred_at_big_sepM. iNext. by iRewrite "HeqP" in "HP". }
   iCombine "Hf" "HP'" as "Hf".
-  rewrite -big_sepM_sepM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
+  rewrite -big_sepM_sep big_opM_fmap; iApply (fupd_big_sepM _ _ f).
   iApply (@big_sepM_impl with "[$Hf]").
   iAlways; iIntros (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
   iInv N as (b) "[>Hγ _]" "Hclose".
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 6f906e018e039d41b277a775b90f774cbdabe15e..7c8d9c738c5da474a840b06ce5eadb119e3b6971 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -301,7 +301,7 @@ Proof. rewrite /lft_dead. iDestruct 1 as (Λ V') "[% H']". set_solver. Qed.
 (* Fractional and AsFractional instances *)
 Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
 Proof.
-  intros p q. rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper=>Λ ?.
+  intros p q. rewrite /lft_tok -big_sepMS_sep. apply big_sepMS_proper=>Λ ?.
   iSplit.
   - iIntros "H". iDestruct "H" as (V') "[#? H] ".
     (* FIXME : the Proper instance for singleton cannot be found automatically here. *)
@@ -321,7 +321,7 @@ Proof. split. done. apply _. Qed.
 Lemma lft_tok_split_obj `{LatBottom Lat bot} q1 q2 κ :
   (q1 + q2).[κ] -∗ q1.[κ] ∗ <obj> q2.[κ].
 Proof.
-  rewrite /lft_tok. rewrite -monPred_objectively_big_sepMS_entails -big_sepMS_sepMS.
+  rewrite /lft_tok. rewrite -monPred_objectively_big_sepMS_entails -big_sepMS_sep.
   apply big_sepMS_mono=>// Λ ?. iStartProof (iProp _). iDestruct 1 as (V) "[#? H]".
   rewrite (fin_maps.singleton_proper Λ _ (Cinl (_, to_latT V ⋅ to_latT bot))); last first.
   { rewrite lat_op_join' right_id //. } rewrite -pair_op -Cinl_op -op_singleton.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index a3ffe31ebc2619f0a82e62fca5bd473dae18a45e..8f19003cbe776eaf07c205e8ead5a156fbb96add 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -60,7 +60,7 @@ Section lft_contexts.
   Global Arguments llctx_interp _ _%Qp.
   Global Instance llctx_interp_fractional L :
     Fractional (llctx_interp L).
-  Proof. intros ??. rewrite -big_sepL_sepL. by setoid_rewrite <-fractional. Qed.
+  Proof. intros ??. rewrite -big_sepL_sep. by setoid_rewrite <-fractional. Qed.
   Global Instance llctx_interp_as_fractional L q :
     AsFractional (llctx_interp L q) (llctx_interp L) q.
   Proof. split. done. apply _. Qed.