update dependencies; fix unification problems

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

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:

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.