diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 8278a042b51c13e0b88f431650f4dae883429eb5..bd06b9058a06e5dc2c073595cd7f46ca714ef237 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.2022-07-05.1.34861bff") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2022-08-12.0.fd801c97") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 237f230d3ae4ae713277865141a75e27e62006e1..e945fae52f40859271ac050a979233efc9dd1b17 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -451,7 +451,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 Pos.add_comm Qp_add_comm -pos_op_plus /= -frac_op pair_op Some_op.
+ rewrite Pos.add_comm Qp_add_comm -pos_op_add /= -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').
@@ -480,7 +480,7 @@ Section ArcGhost.
apply prod_update; simpl; [|by rewrite right_id].
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 /=
+ rewrite Pos.add_comm Qp_add_comm -pos_op_add /=
-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].
@@ -508,7 +508,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_add /= (cmra_comm_L q) pair_op Some_op.
by apply (cancel_local_update_unit (Some _)), _.
Qed.
@@ -532,7 +532,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_add /= (cmra_comm_L q) pair_op Cinl_op Some_op.
by apply (cancel_local_update_unit (Some _)), _.
Qed.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 32472fbf770a4226dbaf6aee66c6561268d42a30..6bf57750cfd7ad4e3ea45e6675ba99b80d088e51 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -96,7 +96,7 @@ Section fn.
{ intros Hprop. apply Hprop, list_fmap_ne; last first.
- symmetry. eapply Forall2_impl; first apply Hfp. intros.
apply dist_later_dist, type_dist2_dist_later. done.
- - apply _. }
+ - solve_proper. }
clear. intros n tid p i x y. rewrite list_dist_lookup=>/(_ i).
case _ : (x !! i)=>[tyx|]; case _ : (y !! i)=>[tyy|];
inversion_clear 1; [solve_proper|done].
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index fc119a2e86121a0d03b16c0b709edf9fc4fcc93c..478fc41f3e87034631aa8ca1b6c807ec7fb0cf15 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -375,7 +375,7 @@ Section code.
(?&?&[=]&?)]]; first done. setoid_subst.
iDestruct "Hproto" as (q'') "(Hl1 & Hl2 & Hl†& >Hqq' & Hν & Hν†)".
iDestruct "Hqq'" as %Hqq'. wp_read. iApply "HΦ". iFrame "Hl1". iRight.
- iSplit; first by rewrite !pos_op_plus; auto with lia. iSplit; iIntros "H↦".
+ iSplit; first by rewrite !pos_op_add; auto with lia. iSplit; iIntros "H↦".
* iMod ("Hclose" with "[- Htok Hν1]") as "$"; last by auto 10 with iFrame.
iFrame. iExists _. iFrame. auto with iFrame.
* iMod (own_update_2 with "Hst Htok") as "Hst".
@@ -385,7 +385,7 @@ Section code.
iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
iSplitL; first last.
{ rewrite [(_+_)%Qp]assoc [(q'+_)%Qp]comm. auto. }
- rewrite pos_op_plus Z.sub_1_r -Pos2Z.inj_pred; last lia.
+ rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
by rewrite Pos.add_1_l Pos.pred_succ.
Qed.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 06d306a1f9935e3611864c422e69e76770e7f312..f14d2a774f9e1f27130f190f9171154b106cfdca 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -172,7 +172,7 @@ Section ref_functions.
iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
- simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame.
iAssert (lrc ↦ #(Z.pos n'))%I with "[H↦lrc]" as "$".
- { rewrite pos_op_plus Z.sub_1_r -Pos2Z.inj_pred; last lia.
+ { rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
by rewrite Pos.add_1_l Pos.pred_succ. }
iMod (own_update with "Hâ—â—¯") as "$".
{ apply auth_update_dealloc.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index d6d019f794a6127e51b8b2291f664373fbf4b287..b4faa81abb0a5215ac0a55402ed70bdbbf2c346d 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -147,7 +147,7 @@ Section refmut_functions.
apply (cancel_local_update_unit (writing_stR q _)), _. }
iDestruct "INV" as "(H†& Hq & _)".
rewrite /= (_:Z.neg (1%positive â‹… n') + 1 = Z.neg n');
- last (rewrite pos_op_plus; lia). iFrame.
+ last (rewrite pos_op_add; lia). iFrame.
iApply step_fupd_intro; [set_solver+|]. iSplitL; [|done].
iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
rewrite assoc (comm _ q'' q) //. }
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index ec6c4eba61599e965150207957cd21a5d2720f4f..73ed9c4e104e5c6ac5a54d854bfa6102ebf1a152 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -71,7 +71,7 @@ Section rwlock_inv.
Proof.
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 /=
+ rewrite Pos.add_comm Qp_add_comm -pos_op_add /=
-{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, _)))).
@@ -144,7 +144,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_add /= (cmra_comm_L q)
-{1}(agree_idemp (to_agree _)) 2!pair_op Cinr_op Some_op.
by apply (cancel_local_update_unit (Some _)), _.
Qed.