bump Iris, adjust for TCEq changes

opam

@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-02-25.0.55283d57") | (= "dev") }
+  "coq-iris" { (= "dev.2020-02-25.3.bb9152ec") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/typing/lib/mutex/mutexguard.v

@@ -252,7 +252,7 @@ Section code.
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hclose4]".
     wp_bind (!_)%E. iApply (wp_step_fupd with "[Hshr Hα2β]");
-         [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+         [|by iApply ("Hshr" with "[] Hα2β")|]; first done.
     wp_read. iIntros "[#Hshr Hα2β] !>". wp_let.
     iDestruct ("Hclose4" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hclose3" with "Hβ HL") as "HL".

theories/typing/lib/rc/rc.v

@@ -695,7 +695,7 @@ Section code.
     - subst strong. wp_op. wp_if. wp_op.
       rewrite shift_loc_0. wp_write. wp_bind (#☠;;#☠)%E.
       iApply (wp_step_fupd with "[Hproto Hrc]");
-        [| |by iApply ("Hproto" with "Hrc")|];
+        [|by iApply ("Hproto" with "Hrc")|];
         [done..|wp_seq; iIntros "(Hty&H†&Hna&Hproto) !>"].
       rewrite <-freeable_sz_full_S, <-(freeable_sz_split _ 2 ty.(ty_size)).
       iDestruct "H†" as "[H†1 H†2]". wp_seq. wp_bind (_<-_;;_)%E.
@@ -790,7 +790,7 @@ Section code.
     iDestruct "Hc" as "[[% [_ Hproto]]|[% [_ Hproto]]]".
     - subst strong. wp_bind (#1 = #1)%E.
       iApply (wp_step_fupd with "[Hproto Hrc]");
-        [| |by iApply ("Hproto" with "Hrc")|];
+        [|by iApply ("Hproto" with "Hrc")|];
         [done..|wp_op; iIntros "(Hty&H†&Hna&Hproto) !>"; wp_if].
       rewrite <-freeable_sz_full_S, <-(freeable_sz_split _ 2 ty.(ty_size)).
       iDestruct "H†" as "[H†1 H†2]". wp_bind (_<-_;;_)%E.

theories/typing/lib/refcell/refmut_code.v

@@ -36,7 +36,7 @@ Section refmut_functions.
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
     wp_bind (!#lx')%E. iApply (wp_step_fupd with "[Hα2β]");
-         [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+         [|by iApply ("Hshr" with "[] Hα2β")|]; first done.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β] !>". wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
@@ -152,7 +152,7 @@ Section refmut_functions.
         iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
         rewrite assoc (comm _ q'' q) //. }
     wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN)); first done.
-    iApply (wp_step_fupd with "INV"); [done|set_solver|]. wp_seq. iIntros "{Hb} Hb !>".
+    iApply (wp_step_fupd with "INV"); [set_solver|]. wp_seq. iIntros "{Hb} Hb !>".
     iMod ("Hcloseβ" with "Hb Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]

theories/typing/lib/rwlock/rwlockreadguard_code.v

@@ -119,7 +119,7 @@ Section rwlockreadguard_functions.
           { rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
           rewrite {1}EQn -{1}(agree_idemp (to_agree _)) 2!pair_op Cinr_op Some_op.
           apply (cancel_local_update_unit (reading_st q ν)) , _. }
-      iApply (wp_step_fupd with "INV"). done. set_solver.
+      iApply (wp_step_fupd with "INV"). set_solver.
       iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
       iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
       iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".

theories/typing/lib/rwlock/rwlockwriteguard_code.v

@@ -37,7 +37,7 @@ Section rwlockwriteguard_functions.
       [solve_typing..|].
     iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
     wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hα2β]");
-         [done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
+         [|by iApply ("Hshr" with "[] Hα2β")|]; first done.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_op. wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1". iMod ("Hclose'" with "Hβ HL") as "HL".

theories/typing/programs.v

@@ -168,7 +168,7 @@ Section typing_rules.
     iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
     iApply (wp_mask_mono _ (↑lftN)); first done.
-    iApply (wp_step_fupd with "Hend"). done. set_solver. wp_seq.
+    iApply (wp_step_fupd with "Hend"); first set_solver. wp_seq.
     iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
   Qed.