diff --git a/opam b/opam
index eb9277d056804de96ae9689a09b2a8b441b7d743..61d0d843454fe382efc5c1fae8eac174717326ca 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-09-30.0.50bc07aa") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-10-01.0.7fcd4a3d") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index b0c3e88cd7798d4d01fbaa81fc4f31677748e96d..55b606b065874493a00873bde51123d8e46d2415 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -219,7 +219,7 @@ Section ArcGhost.
     rewrite -embed_sep -own_op.
     iIntros "own". iDestruct (own_valid with "own") as %VAL. iPureIntro.
     move : VAL => [/=_ [/= [[VAL  _]_]_]]. move :VAL.
-    rewrite /= -auth_frag_op -Some_op -pair_op auth_valid_discrete /= Some_valid.
+    rewrite /= -auth_frag_op -Some_op -pair_op auth_frag_valid.
     move => [_ /to_agree_op_inv /to_latT_inj /leibniz_equiv_iff // ].
   Qed.
 
@@ -366,7 +366,7 @@ Section ArcGhost.
     iDestruct 1 as (Ut) "WU". iIntros "WU'".
     iDestruct (WkUps_join with "[$WU $WU']") as "WU".
     iDestruct (@own_valid _ arcUR with "WU")
-      as %[_ [_ [[VAL _]%auth_valid_discrete _]]].
+      as %[_ [_ [[VAL _]%auth_frag_valid _]]].
     iPureIntro. simpl in VAL.
     have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
     apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
@@ -571,7 +571,7 @@ Section ArcGhost.
     rewrite -embed_sep -own_op. iIntros "own".
     iDestruct (@own_valid _ arcUR with "own") as %[[_ VAL] _]. simpl in VAL.
     iPureIntro. move : VAL. rewrite -auth_frag_op -pair_op -Some_op frac_op'.
-    move => /auth_valid_discrete /= [/= ? _].
+    move => /auth_frag_valid /= [/= ? _].
     have Lt: (1%Qp < (1%Qp + q)%Qp)%Qc. apply Qp_lt_sum. by eexists.
     apply (irreflexive_eq (R:= Qclt) 1%Qp 1%Qp); [done|].
     eapply Qclt_le_trans; [apply Lt|done].
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index f10112f59fc89e3c0973806654d9001022f3f23d..dfab5d68d7134f6303556c15950348e8bb99bf9d 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -154,8 +154,9 @@ Proof.
       as %[EQB2%to_borUR_included _]%auth_both_valid_discrete.
   iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
   { iIntros (->).
-    iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
-    exfalso. revert Hj1j2. by rewrite /= singleton_op singleton_valid. }
+    iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2.
+    exfalso. move: Hj1j2. rewrite -auth_frag_op auth_frag_valid.
+    by rewrite /= singleton_op singleton_valid. }
   iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
     as (γ) "(% & Hslice & Hbox)"; first solve_ndisj.
   { done. }
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 112cdaa87304d80528d0fa071ea8213b1404eea4..22409bd2aef568d704817a894677b26e50260bf7 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -16,9 +16,9 @@ Proof.
   destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
   { iModIntro. iExists A, I. iFrame. iPureIntro. by apply elem_of_dom. }
   iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first by apply auth_both_valid_discrete.
-  iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name (excl (bor_state Lat)))))
+  iMod (own_alloc (● (∅ : gmap slice_name (excl (bor_state Lat))) ⋅ ◯ ∅))
     as (γbor) "[Hbor Hbor']"; first by apply auth_both_valid_discrete.
-  iMod (own_alloc ((● ε) :auth (gset_disj slice_name)))
+  iMod (own_alloc (● (ε : gset_disj slice_name)))
      as (γinh) "Hinh"; first by apply auth_auth_valid.
   set (γs := LftNames γbor γcnt γinh).
   iMod (own_update with "HI") as "[HI Hγs]".