diff --git a/opam b/opam
index 203be2403f04a16beafe10bfbfef18e689c6434d..d57c87b261eb65bbdc295d0d2fe82033d4836940 100644
--- a/opam
+++ b/opam
@@ -16,7 +16,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2020-10-10.1.4e05b3e8") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-10-13.0.65e2d7ca") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 55b606b065874493a00873bde51123d8e46d2415..ec4e06cd19c33c0878b938085b22e61788746536 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -436,7 +436,7 @@ Section ArcGhost.
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
     apply prod_update; simpl; [|by rewrite right_id].
     apply prod_update; simpl; [|done]. apply auth_update_alloc.
-    rewrite /= -(right_id None op (Some _)). by apply op_local_update_discrete.
+    rewrite /= -(right_id None op (Some _)). by apply: op_local_update_discrete.
   Qed.
 
   Lemma StrongAuth_new_tok γ (q q': frac) n (Hqq' : (q + q')%Qp = 1%Qp):
@@ -496,7 +496,7 @@ Section ArcGhost.
     apply prod_update; simpl; [|by rewrite right_id].
     apply prod_update; simpl; [|done].
     apply auth_update_dealloc. rewrite /= -(right_id None op (Some _)).
-    apply cancel_local_update_unit, _.
+    apply: cancel_local_update_unit.
   Qed.
 
   Lemma StrongAuth_drop γ q q' n:
@@ -519,7 +519,7 @@ Section ArcGhost.
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
     apply prod_update; [|by rewrite /= right_id]. apply prod_update; [done|].
     apply auth_update_dealloc. apply prod_local_update; [done|].
-    rewrite /= -(right_id None op (Some _)). apply cancel_local_update_unit, _.
+    rewrite /= -(right_id None op (Some _)). apply: cancel_local_update_unit.
   Qed.
 
   Lemma WeakAuth_drop γ iS (q q': frac) n:
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 5dc181dccf5f76f1a6118c02f2bfc65d56c56d2a..6fa28d522b125093d5e27d9ce8593afc2f6be205 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -365,7 +365,7 @@ Section code.
              { by rewrite !Nat2Z.inj_succ -!Z.add_1_l Z.add_simpl_l. }
              iMod (own_update_2 with "Hst Htok") as "$"; last done.
              apply auth_update_dealloc, prod_local_update', reflexivity.
-             rewrite -{1}(right_id None _ (Some _)). apply cancel_local_update_unit, _.
+             rewrite -{1}(right_id None _ (Some _)). apply: cancel_local_update_unit.
       + apply csum_included in Hincl.
         destruct Hincl as [->|[(?&(?,?)&[=<-]&->&(q',strong)&[]%(inj2 pair))|
                                (?&?&[=]&?)]]; first done. setoid_subst.