diff --git a/opam b/opam
index d57c87b261eb65bbdc295d0d2fe82033d4836940..e41b3f1e48e3899425c4e9b647fd9f4fded83a2e 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-10-13.0.65e2d7ca") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-10-21.0.e29403ca") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index ec4e06cd19c33c0878b938085b22e61788746536..81a09112264ad992821c6a1e99d6ac6aaff1d674 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -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_frag_valid _]]].
+      as %[_ [_ [[VAL _]%auth_frag_valid_1 _]]].
     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|].
@@ -583,7 +583,7 @@ Section ArcGhost.
     iDestruct 1 as (Mt) "SM". iIntros "SM'".
     iDestruct (StrMoves_agree with "[$SM $SM']") as %?. subst Mt'.
     iDestruct (StrMoves_fractional with "[$SM $SM']") as "SM".
-    iDestruct (@own_valid _ arcUR with "SM") as %[_ [[[[VAL _] _] _] _]].
+    iDestruct (@own_valid _ arcUR with "SM") as %[_ [[[[VAL _]%auth_frag_valid_1 _] _] _]].
     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|].