update dependencies; solve some unification problems

opam

@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-10-09.1.86125f9c") | (= "dev") }
+  "coq-iris" { (= "dev.2020-10-13.1.5558d66d") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/lang/lib/arc.v

@@ -520,7 +520,7 @@ Section arc.
       + destruct Hqq' as [<- ->].
         iMod (own_update_2 with "H● Hown") as "[H● H◯]".
         { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
-          etrans; first apply cancel_local_update_unit, _.
+          etrans; first apply: cancel_local_update_unit.
           by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
         iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
         iModIntro. wp_case. iApply wp_fupd. wp_op.
@@ -553,7 +553,7 @@ Section arc.
     - wp_apply (wp_cas_int_suc with "Hs"). iIntros "Hs".
       destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
       { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
-        etrans; first apply cancel_local_update_unit, _.
+        etrans; first apply: cancel_local_update_unit.
         by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
       iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
       iApply ("HΦ" $! true). rewrite -{1}Hq''. iFrame. by iApply close_last_strong.
@@ -616,7 +616,7 @@ Section arc.
       + setoid_subst. iDestruct "H" as (?) "(Hq & ? & ? & >? & >%)". subst. wp_read.
         iMod (own_update_2 with "H● H◯") as "H●".
         { apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id.
-          apply cancel_local_update_unit, _. }
+          apply: cancel_local_update_unit. }
         iMod ("Hclose" with "[H●]") as "_"; first by iExists _; iFrame.
         iModIntro. wp_seq. wp_op. wp_let. wp_op. wp_write. iApply "HΦ".
         iDestruct "Hq" as %<-. iFrame.
@@ -644,7 +644,7 @@ Section arc.
     - wp_apply (wp_cas_int_suc with "Hs")=>//. iIntros "Hs".
       destruct Hqq' as [<- ->]. iMod (own_update_2 with "H● Hown") as "[H● H◯]".
       { apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
-        etrans; first apply cancel_local_update_unit, _.
+        etrans; first apply: cancel_local_update_unit.
         by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
       iCombine "HP1" "HP1'" as "HP1". rewrite Hq''. clear Hq'' q''.
       iMod ("Hclose" with "[H● Hs Hw]") as "_"; first by iExists _; do 2 iFrame.

theories/typing/lib/rc/rc.v

@@ -294,7 +294,7 @@ Section code.
           -- iLeft. iSplit; first done. rewrite Hincls. iFrame "Hl†".
              iMod (own_update_2 with "Hst Htok") as "Hst".
              { apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
-               apply cancel_local_update_unit, _. }
+               apply: cancel_local_update_unit. }
              rewrite -[in (1).[ν]%I]Hqq' -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans.
              iApply step_fupd_mask_mono;
                last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
@@ -329,7 +329,7 @@ Section code.
         * iIntros "Hl1".
           iMod (own_update_2 with "Hst Htok") as "[Hst Htok]".
           { apply auth_update. etrans.
-            - rewrite [(Some _, weak)]pair_split. apply cancel_local_update_unit, _.
+            - rewrite [(Some _, weak)]pair_split. apply: cancel_local_update_unit.
             - apply (op_local_update _ _ (Some (Cinr (Excl tt)), 0%nat)). auto. }
           rewrite -[(|={↑lft_userN,⊤}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'.
           iApply step_fupd_mask_mono;
@@ -356,14 +356,14 @@ Section code.
              iApply ("Hclose" with "[>- $Hna]"). iExists (None, 0%nat).
              iMod (own_update_2 with "Hst Htok") as "$"; last done.
              apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
-             apply cancel_local_update_unit, _.
+             apply: cancel_local_update_unit.
           -- iRight. iSplitR; first by auto with lia. iIntros "!> Hl† Hl2 Hvl".
              iApply ("Hclose" with "[>- $Hna]"). iExists (None, S weak).
              rewrite Hincls. iFrame. iSplitR "Hl2"; last first.
              { 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.