diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index e17cdd0a8954b5d88aa8454be34c14477e28cc89..6e7efb62cfe29b151ceee1175b863c7fcea8571c 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-01-26.2.79f2f36f") | (= "dev") }
+  "coq-iris" { (= "dev.2021-02-10.0.7b4a04ce") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 90d563baab5779278648fe4f835eeef695881b1e..c648706c0f089ae54f818a353d90d26f1d0b66f1 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -274,12 +274,12 @@ Section arc.
       { apply auth_update_alloc, prod_local_update_1,
          (op_local_update_discrete _ _ (Some (Cinl ((qq/2)%Qp, 1%positive, None))))
            =>-[/= Hqa ?]. split;[split|]=>//=; last by rewrite left_id.
-        apply frac_valid'. rewrite -Hq comm_L.
+        apply frac_valid. rewrite -Hq comm_L.
         by apply Qp_add_le_mono_l, Qp_div_le. }
       iMod ("Hclose2" with "Hown") as "HP". iModIntro.
       iMod ("Hclose1" with "[Hl Hw H● HP1']") as "_".
       { iExists _. iFrame. iExists _. rewrite /= [xH â‹… _]comm_L. iFrame.
-        rewrite [(qq / 2)%Qp â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
+        rewrite [(qq / 2)%Qp â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp_div_2 left_id_L. auto. }
       iModIntro. wp_case. iApply "HΦ". iFrame.
     - wp_apply (wp_cas_int_fail with "Hl"); [congruence|]. iIntros "Hl".
       iMod ("Hclose2" with "Hown") as "HP". iModIntro.
@@ -405,10 +405,10 @@ Section arc.
           { apply auth_update_alloc. rewrite -[(_,0%nat)]right_id.
             apply op_local_update_discrete=>Hv. constructor; last done.
             split; last by rewrite /= left_id; apply Hv. split=>[|//].
-            apply frac_valid'. rewrite /= -Heq comm_L.
+            apply frac_valid. rewrite /= -Heq comm_L.
             by apply Qp_add_le_mono_l, Qp_div_le. }
           iFrame. iApply "Hclose1". iExists _. iFrame. iExists _. iFrame.
-          rewrite /= [xH â‹… _]comm_L frac_op' [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
+          rewrite /= [xH â‹… _]comm_L frac_op [(_ + c)%Qp]comm -[(_ + _)%Qp]assoc
                   Qp_div_2 left_id_L. auto with iFrame.
         + iIntros "Hl". iFrame. iApply ("Hclose1" with "[-]"). iExists _. iFrame.
           iExists q. auto with iFrame.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 8d85d84c87b6fe2494a40fd4e8e531d01c35f321..721a53a4f786185d85007a095779d376df988412 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -94,7 +94,7 @@ Proof.
     iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
     iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
     rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
-  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
+  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op auth_frag_op own_cnt_op.
   by iFrame.
 Qed.
 
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 30f9e0d1b05e790f7af14d4d49ef273dc87fc453..a02cd0c7bf23a6d0a1c33b1ec8bd40893e92e6f8 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -590,13 +590,13 @@ Section code.
     iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
     { apply auth_update_alloc, prod_local_update_1,
       (op_local_update_discrete _ _ (Some (Cinl ((qb/2)%Qp, 1%positive))))=>-[/= Hqa _].
-      split; simpl; last done. apply frac_valid'. rewrite /= -H comm_L.
+      split; simpl; last done. apply frac_valid. rewrite /= -H comm_L.
       by apply Qp_add_le_mono_l, Qp_div_le. }
     rewrite right_id -Some_op -Cinl_op -pair_op. iDestruct "Hνtok" as "[Hνtok1 Hνtok2]".
     iMod ("Hclose3" with "[$Hrctok] Hna") as "[Hα1 Hna]".
     iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hνtok2 Hν† $Hna]") as "Hna".
     { iExists _. iFrame "Hrc●". iExists _. rewrite Z.add_comm. iFrame.
-      rewrite [_ â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2. auto. }
+      rewrite [_ â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp_div_2. auto. }
     iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ x ◁ box (&shr{α}(rc ty)); #lr ◁ box (rc ty)]
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 987eb1b9e4e194bd57b28228d876c27ef2aec050..91b5c4e0f08eeb68925c963d92be0e67b78fedf1 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -167,13 +167,13 @@ Section code.
       iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
       { apply auth_update_alloc, prod_local_update_1,
         (op_local_update_discrete _ _ (Some (Cinl ((qb/2)%Qp, 1%positive))))=>-[/= Hqa _].
-        split; simpl; last done. apply frac_valid'.
+        split; simpl; last done. apply frac_valid.
         rewrite /= -Hq''q0 comm_L. by apply Qp_add_le_mono_l, Qp_div_le. }
       rewrite right_id -Some_op -Cinl_op -pair_op.
       iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
       iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 Hl'† Hν2 Hν† $Hna]") as "Hna".
       { iExists _. iFrame "Hrc●". iExists _. rewrite Z.add_comm. iFrame.
-        rewrite [_ â‹… _]comm frac_op' -[(_ + _)%Qp]assoc Qp_div_2. auto. }
+        rewrite [_ â‹… _]comm frac_op -[(_ + _)%Qp]assoc Qp_div_2. auto. }
       iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
       (* Finish up the proof. *)
       iApply (type_type _ _ _ [ w ◁ box (&shr{α}(weak ty)); #lr ◁ box (uninit 2);
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index bf9ac8b1e12b305e4f95d7718b67079f4d317a8f..27baff9cf46b087c43ceb286d4e5ee6d12dd182d 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -73,7 +73,7 @@ Section ref_functions.
          (op_local_update_discrete _ _ (reading_stR (q''/2)%Qp ν))=>-[Hagv _].
       split; [split|done].
       - by rewrite /= agree_idemp.
-      - apply frac_valid'. rewrite /= -Hq'q'' comm_L.
+      - apply frac_valid. rewrite /= -Hq'q'' comm_L.
         by apply Qp_add_le_mono_l, Qp_div_le. }
     wp_apply wp_new; [done..|]. iIntros (lr) "(?&Hlr)".
     iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I  with "[H↦1 H↦2]" as "H↦".
@@ -335,7 +335,7 @@ Section ref_functions.
          (op_local_update_discrete _ _ (reading_stR (q2/2)%Qp ν))=>-[Hagv _].
       split; [split|done].
       - by rewrite /= agree_idemp.
-      - apply frac_valid'. rewrite /= -Hq1q2 comm_L.
+      - apply frac_valid. rewrite /= -Hq1q2 comm_L.
         by apply Qp_add_le_mono_l, Qp_div_le. }
     wp_let. wp_read. wp_let. wp_op. wp_write.
     wp_apply (wp_delete _ _ _ [_; _] with "[Href↦1 Href↦2 Href†]")=>//.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 6bda8af9ade8049703a2260056c41c152660ba19..881ba5c63b923cd25b0e9668fa737f656cbd289d 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -184,7 +184,7 @@ Section refcell_functions.
               (op_local_update_discrete _ _ (reading_stR (q'/2)%Qp ν)) => ?.
             split; [split|].
             - by rewrite /= agree_idemp.
-            - apply frac_valid'. rewrite /= -Hqq' comm_L.
+            - apply frac_valid. rewrite /= -Hqq' comm_L.
               by apply Qp_add_le_mono_l, Qp_div_le.
             - done. }
           iFrame "∗#". iExists (Some (ν, false, _, _)). iFrame "∗#".
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 25ade67a3f5213222ab53e7812623d4a27ea7545..2a32ac07d8274fca8e109f37b5cf78c8e20da255 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -309,7 +309,7 @@ Section refmut_functions.
          (op_local_update_discrete _ _ (writing_stR (q1/2)%Qp ν))=>-[Hagv _].
       split; [split|done].
       - by rewrite /= agree_idemp.
-      - apply frac_valid'. rewrite /= -Hqq1 comm_L.
+      - apply frac_valid. rewrite /= -Hqq1 comm_L.
         by apply Qp_add_le_mono_l, Qp_div_le. }
     wp_let. wp_read. wp_let. wp_op. wp_write.
     wp_apply (wp_delete _ _ _ [_; _] with "[Hrefmut↦1 Hrefmut↦2 Hrefmut†]")=>//.
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 2e1340a2e8c3132a2b6190561d4d03761aa420d9..175cf68c9ba825498a1b34008232c79be14585f5 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -193,7 +193,7 @@ Section rwlock_functions.
               (op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
               split; [split|].
               - by rewrite /= Hag agree_idemp.
-              - apply frac_valid'. rewrite /= -Hqq' comm_L.
+              - apply frac_valid. rewrite /= -Hqq' comm_L.
                 by apply Qp_add_le_mono_l, Qp_div_le.
               - done. }
             iFrame "∗#". iExists _. rewrite Z.add_comm /=. iFrame. iExists _, _.