update dependencies; fix for auth changes

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

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|].