diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index d17814897691803b63a9817c12dc05267746764a..1e1cc123ea39d8d68b88dd7346d4bd240f50440e 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-01-25.0.04d22616") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-02-11.0.9fc05451") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 49478dc2434de287c8961bcbfcf3167cb0993f03..9c215c85bf8ee1b7ea47d84afc402f841b7d389f 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -154,7 +154,7 @@ Section ArcGhost.
     rewrite /Fractional => p q. rewrite -embed_sep -own_op.
     apply embed_proper, own.own_proper.
     apply pair_proper; [done|]. do 3 (apply pair_proper; [|done]). simpl.
-    by rewrite -auth_frag_op -Some_op -pair_op frac_op' agree_idemp.
+    by rewrite -auth_frag_op -Some_op -pair_op frac_op agree_idemp.
   Qed.
   Global Instance StrMoves_asfractional γ q Mt :
     AsFractional (StrMoves γ q Mt) (λ q, StrMoves γ q Mt) q.
@@ -166,7 +166,7 @@ Section ArcGhost.
     apply pair_proper; [done|]. apply pair_proper; [|done].
     rewrite /=. setoid_rewrite <-pair_op. apply pair_proper; [done|].
     rewrite -pair_op. apply pair_proper; [|done].
-    by rewrite -auth_frag_op -Some_op -pair_op frac_op' lat_op_join' lat_join_idem_L.
+    by rewrite -auth_frag_op -Some_op -pair_op frac_op lat_op_join' lat_join_idem_L.
   Qed.
   Global Instance StrDowns_asfractional γ q Dt :
     AsFractional (StrDowns γ q Dt) (λ q, StrDowns γ q Dt) q.
@@ -177,7 +177,7 @@ Section ArcGhost.
     apply embed_proper, own.own_proper.
     do 2 (apply pair_proper; [done|]).
     rewrite /=. setoid_rewrite <-pair_op. apply pair_proper; [|done].
-    by rewrite -auth_frag_op -Some_op -pair_op frac_op' lat_op_join' lat_join_idem_L.
+    by rewrite -auth_frag_op -Some_op -pair_op frac_op lat_op_join' lat_join_idem_L.
   Qed.
   Global Instance WkUps_asfractional γ q Ut :
     AsFractional (WkUps γ q Ut) (λ q, WkUps γ q Ut) q.
@@ -293,7 +293,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
     do 2 (apply pair_proper; [done|]; apply pair_proper; [|done]).
-    simpl. rewrite -auth_frag_op -Some_op -pair_op -frac_op' lat_op_join'.
+    simpl. rewrite -auth_frag_op -Some_op -pair_op -frac_op lat_op_join'.
     rewrite (lat_le_join_l_L (Dt ∪ Dt') Dt'); [done|solve_lat].
   Qed.
 
@@ -319,7 +319,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
     do 2 (apply pair_proper; [done|]). apply pair_proper; [|done]. simpl.
-    rewrite -auth_frag_op -Some_op -pair_op -frac_op' lat_op_join'.
+    rewrite -auth_frag_op -Some_op -pair_op -frac_op lat_op_join'.
     rewrite (lat_le_join_l_L (Ut ∪ Ut') Ut'); [done|solve_lat].
   Qed.
 
@@ -329,7 +329,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. apply embed_proper, own.own_proper.
     do 2 (apply pair_proper; [done|]; apply pair_proper; [|done]).
-    simpl. by rewrite -auth_frag_op -Some_op -pair_op -frac_op' lat_op_join'.
+    simpl. by rewrite -auth_frag_op -Some_op -pair_op -frac_op lat_op_join'.
   Qed.
 
   Lemma StrDowns_update γ Dt1 Dt2 Dt' q :
@@ -402,7 +402,7 @@ Section ArcGhost.
     inversion Eq1. subst q1. exists q', n. split; [done|].
     destruct Eq3 as [[Eq3 Eq4]|[[q'' Le1] Le2%pos_included]%prod_included].
     - inversion Eq3. inversion Eq4. simpl in *. by subst.
-    - simpl in *. rewrite decide_False. exists q''. by rewrite Le1 frac_op'.
+    - simpl in *. rewrite decide_False. exists q''. by rewrite Le1 frac_op.
       move => ?. by subst n.
   Qed.
 
@@ -425,7 +425,7 @@ Section ArcGhost.
       subst qn. exists q', weak, st'. split; [done|]. inversion Eq2. subst.
       apply prod_included in INCL as [[q'' Eq] INCLs%pos_included]. simpl in *.
       rewrite decide_False.
-      exists q''. by rewrite Eq frac_op'. move => ?. by subst weak.
+      exists q''. by rewrite Eq frac_op. move => ?. by subst weak.
   Qed.
 
   Lemma StrongAuth_first_tok γ :
@@ -448,10 +448,10 @@ 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 Pos.add_comm Qp_add_comm -pos_op_plus /= -frac_op' pair_op Some_op.
+    rewrite Pos.add_comm Qp_add_comm -pos_op_plus /= -frac_op pair_op Some_op.
     rewrite -{2}(right_id None op (Some ((q' /2)%Qp, _))).
     apply op_local_update_discrete => _ /=. split; simpl; [|done].
-    apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
+    apply frac_valid. rewrite -Hqq' comm -{2}(Qp_div_2 q').
     apply Qp_add_le_mono_l. apply Qp_le_add_r.
   Qed.
 
@@ -478,10 +478,10 @@ Section ArcGhost.
     apply prod_update; simpl; [done|]. apply auth_update_alloc.
     apply prod_local_update; simpl; [done|].
     rewrite Pos.add_comm Qp_add_comm -pos_op_plus /=
-            -frac_op' pair_op Cinl_op Some_op.
+            -frac_op pair_op Cinl_op Some_op.
     rewrite -{2}(right_id None op (Some $ Cinl ((q' /2)%Qp, _))).
     apply op_local_update_discrete => _ /=. split; simpl; [|done].
-    apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q').
+    apply frac_valid. rewrite -Hqq' comm -{2}(Qp_div_2 q').
     apply Qp_add_le_mono_l. apply Qp_le_add_r.
   Qed.
 
@@ -505,7 +505,7 @@ Section ArcGhost.
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
     apply prod_update; [|simpl; by rewrite right_id]. apply prod_update; [|done].
     apply auth_update_dealloc.
-    rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q) pair_op Some_op.
+    rewrite -frac_op -pos_op_plus /= (cmra_comm_L q) pair_op Some_op.
     by apply (cancel_local_update_unit (Some _)), _.
   Qed.
 
@@ -529,7 +529,7 @@ Section ArcGhost.
     iMod (@own_update _ arcUR with "own") as "$"; [|done].
     apply prod_update; [|simpl; by rewrite right_id]. apply prod_update; [done|].
     apply auth_update_dealloc. apply prod_local_update; [done|].
-    rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q) pair_op Cinl_op Some_op.
+    rewrite -frac_op -pos_op_plus /= (cmra_comm_L q) pair_op Cinl_op Some_op.
     by apply (cancel_local_update_unit (Some _)), _.
   Qed.
 
@@ -568,7 +568,7 @@ Section ArcGhost.
   Proof.
     rewrite -embed_sep -own_op. iIntros "own".
     iDestruct (@own_valid _ arcUR with "own") as %[[_ VAL] _]. simpl in VAL.
-    iPureIntro. move : VAL. rewrite -auth_frag_op -pair_op -Some_op frac_op'.
+    iPureIntro. move : VAL. rewrite -auth_frag_op -pair_op -Some_op frac_op.
     move => /auth_frag_valid /= [/= ? _].
     have Lt: (1 < 1 + q)%Qp. apply Qp_lt_sum. by eexists.
     apply (irreflexive_eq (R:= Qp_lt) 1%Qp 1%Qp); [done|].
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index b0fec12b97438bd7188f9a6922d10b417fd692c7..e852ec895585f275608d0e6bea3cd9671a07c462 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -124,14 +124,14 @@ Section frac_bor.
     iAssert (▷ ⎡own γ qq⎤ ∗
              ▷ ⎡own γ (qφ0' + qφ0 / 2 ⋅? qφ1)%Qp⎤)%I with "[Hown]" as "[>Hown1 Hown2]".
     { rewrite -bi.later_sep -embed_sep -own_op. iNext.
-      by rewrite -!frac_op' -!cmra_op_opM_assoc_L assoc_L !frac_op' -Hqφ Qp_div_2. }
+      by rewrite -!frac_op -!cmra_op_opM_assoc_L assoc_L !frac_op -Hqφ Qp_div_2. }
     rewrite monPred_objectively_unfold Hqκ'. iDestruct ("Hκ2" $! V0) as "[Hκ2 Hκ2']".
     iMod ("Hclose'" with "[-Hown1 Hclose Hκ2']") as "Hκ1".
     { iIntros "#HVb". iExists (qφ0' + qφ0 / 2)%Qp, (qtok ⋅ Some qq)%Qp, qφ1.
       iNext. iFrame. iSplit; [|iSplitR "Hφ1"].
       - iPureIntro.
         rewrite (comm_L _ qtok) cmra_opM_opM_assoc_L -assoc_L Some_op_opM /=.
-        rewrite -cmra_op_opM_assoc_L frac_op' -(comm_L _ qq) assoc_L -Hqφ Qp_div_2.
+        rewrite -cmra_op_opM_assoc_L frac_op -(comm_L _ qq) assoc_L -Hqφ Qp_div_2.
         by rewrite -cmra_opM_opM_assoc_L.
       - rewrite comm_L Some_op_opM. destruct qtok as [qtok|]; simpl; [|done].
         by iSplitL "Hκ2".
@@ -154,7 +154,7 @@ Section frac_bor.
     assert (∃ qm, qtok = qq ⋅? qm)%Qp as [qm ->].
     { assert (qq ≤ qtok)%Qp as [[qm ->]%Qp_lt_sum| ->]%Qp_le_lteq.
       - rewrite (Qp_add_le_mono_r _ _ (qφ0 ⋅? qφ1)). trans 1%Qp; [done|].
-        apply reflexive_eq. by rewrite -frac_op' -cmra_op_opM_assoc_L comm_L.
+        apply reflexive_eq. by rewrite -frac_op -cmra_op_opM_assoc_L comm_L.
       - by exists (Some qm).
       - by exists None. }
     iAssert (⎡from_option (λ qm', qm'.[κ']) True qm V0⎤ ∗ ⎡ monPred_at qq.[κ'] V0 ⎤)%I
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 503112e9ea1ce686701664395dc5d37e37453085..80592d5d2315c92732dc5cf059c42a71d57593f2 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -147,7 +147,7 @@ Proof.
     iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
     iExists (<[i:=Bor_in VP]>B'). rewrite /to_borUR !fmap_insert. iFrame.
     rewrite -insert_delete big_sepM_insert ?lookup_delete //=. iFrame. auto. }
-  rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op. by iFrame.
+  rewrite -[S n]Nat.add_1_l -nat_op auth_frag_op own_cnt_op. by iFrame.
 Qed.
 
 Lemma raw_idx_bor_unnest E κ κ' i P :
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 480be65c73ba942e65f0de32e86e7cbf133da34a..6e46c823737a2f649a31df83dd4bf22a2e0f2aea 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -593,13 +593,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 210720639a03e8dd5289e3420bf247043b28a530..0195aa92e9c791c607ec8b747a30ff2bc1f17476 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -173,13 +173,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 62f4a49f6b224f47df71435daa0dd3c148d7730b..583d03407a613cab176170549649421b45e8dcea 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -72,7 +72,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↦".
@@ -334,7 +334,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 21e4ca17decdbcba89cfcfe61d2243873a2efdb8..e6aa46e9db7ac380ac045f303f8ed37eb21de089 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -183,7 +183,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 424ab2ba1cb9914549e6d3f682bba88a007b3d16..550751122920464cf292fe1c9dcf0574f33eec34 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -307,7 +307,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.v b/theories/typing/lib/rwlock/rwlock.v
index 9976bcfceda4cdc014a502ab210328560dc1598c..a36127024919eb8515a2e4b1632db9d32e5b7ba5 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -71,12 +71,12 @@ Section rwlock_inv.
     iIntros (st') "g". rewrite -embed_sep -own_op.
     iMod (own_update with "g") as "$"; [|done]. apply auth_update_alloc.
     rewrite Pos.add_comm Qp_add_comm -pos_op_plus /=
-            -{2}(agree_idemp (to_agree _)) -frac_op'
+            -{2}(agree_idemp (to_agree _)) -frac_op
             2!pair_op Cinr_op Some_op.
     rewrite -{2}(right_id None op (Some (Cinr (_, (q' /2)%Qp, _)))).
     apply op_local_update_discrete =>-[Hagv _]. split; [split|done].
     - by rewrite /= agree_idemp.
-    - apply frac_valid'. rewrite -Hqq' comm -{2}(Qp_div_2 q') /=.
+    - apply frac_valid. rewrite -Hqq' comm -{2}(Qp_div_2 q') /=.
       apply Qp_add_le_mono_l. apply Qp_le_add_r.
   Qed.
 
@@ -120,7 +120,7 @@ Section rwlock_inv.
         apply prod_included in INCL as
           [[INCL%to_agree_included LE1]%prod_included LE2%pos_included].
         inversion INCL. do 2 eexists. split; [done|]. right. split.
-        * rewrite /= in LE1. destruct LE1 as [q1 LE1]. exists q1. by rewrite -frac_op'.
+        * rewrite /= in LE1. destruct LE1 as [q1 LE1]. exists q1. by rewrite -frac_op.
         * rewrite -Pplus_one_succ_l Pos.succ_pred => //?. by subst.
     - by apply option_included in INCL as [?|[?[?[?[??]]]]].
   Qed.
@@ -143,7 +143,7 @@ Section rwlock_inv.
     iIntros "m r". iCombine "m" "r" as "mr".
     iMod (own_update with "mr") as "$"; [|done].
     apply auth_update_dealloc.
-    rewrite -frac_op' -pos_op_plus /= (cmra_comm_L q)
+    rewrite -frac_op -pos_op_plus /= (cmra_comm_L q)
             -{1}(agree_idemp (to_agree _)) 2!pair_op Cinr_op Some_op.
     by apply (cancel_local_update_unit (Some _)), _.
   Qed.