diff --git a/theories/examples/namegen.v b/theories/examples/namegen.v
index 494c19608567519be9433bddde7ebb8542511814..890d79c84f7d7073c379306d226125f966b16237 100644
--- a/theories/examples/namegen.v
+++ b/theories/examples/namegen.v
@@ -64,7 +64,7 @@ Section namegen_refinement.
{ iIntros (Hy). destruct Hy as [y Hy].
rewrite (big_sepS_elem_of _ L (l',y) Hy).
iDestruct "HL" as "[Hl _]".
- iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %Hfoo.
+ iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %[Hfoo _].
compute in Hfoo. eauto. }
iAssert (⌜(∃ x, (x, S n) ∈ L) → FalseâŒ)%I with "[HL]" as %Hc.
{ iIntros (Hx). destruct Hx as [x Hy].
diff --git a/theories/examples/par.v b/theories/examples/par.v
index 1874fa496a24a401ffe52ae914676e35c34fe66a..12d463a2f7a9258b20892a0277a5a827e1dfe29e 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -108,38 +108,41 @@ Section rules.
rel_values.
Qed.
- (* Lemma par_l_1' Q K e1 e2 t : *)
- (* (REL e1 << t : ()) -∗ *)
- (* (WP e2 {{ _, Q }}) -∗ *)
- (* (Q -∗ REL #() << fill K (#() : expr) : ()) -∗ *)
- (* REL (e1 ∥ e2) << fill K t : (). *)
- (* Proof. *)
- (* iIntros "He1 He2 Ht". *)
- (* rel_pures_l. rel_rec_l. *)
- (* rel_pures_l. *)
- (* pose (N:=nroot.@"par"). *)
- (* rewrite {1 3}refines_eq /refines_def. iIntros (j K') "#Hspec Hj". *)
- (* iModIntro. wp_bind (spawn _). *)
- (* iApply (spawn_spec N (λ _, j ⤇ fill (K++K') #())%I with "[He1 Hj]"). *)
- (* - wp_pures. wp_bind e1. *)
- (* rewrite -fill_app. *)
- (* iMod ("He1" with "Hspec Hj") as "He1". *)
- (* iApply (wp_wand with "He1"). *)
- (* iIntros (?) "P". wp_pures. *)
- (* by iDestruct "P" as (v') "[Hj [-> ->]]". *)
- (* - iNext. iIntros (l) "hndl". iSimpl. *)
- (* wp_pures. wp_bind e2. *)
- (* iApply (wp_wand with "He2"). iIntros (?) "HQ". *)
- (* wp_pures. *)
- (* wp_apply (join_spec with "hndl"). *)
- (* iIntros (?) "Hj". *)
- (* iSpecialize ("Ht" with "HQ"). *)
- (* rewrite refines_eq /refines_def. *)
- (* rewrite fill_app. *)
- (* iMod ("Ht" with "Hspec Hj") as "Ht". *)
- (* rewrite wp_value_inv. iMod "Ht" as (?) "[Ht [_ ->]]". *)
- (* wp_pures. iExists #(). eauto with iFrame. *)
- (* Qed. *)
+ Lemma par_l_1' Q K e1 e2 t :
+ (REL e1 << t : ()) -∗
+ (WP e2 {{ _, Q }}) -∗
+ (Q -∗ REL #() << fill K (#() : expr) : ()) -∗
+ REL (e1 ∥ e2) << fill K t : ().
+ Proof.
+ iIntros "He1 He2 Ht".
+ rel_pures_l. rel_rec_l.
+ rel_pures_l.
+ pose (N:=nroot.@"par").
+ iApply refines_split. iIntros (k) "Hk".
+ rel_bind_l (spawn _). iApply refines_wp_l.
+ rewrite refines_right_bind.
+ iApply (spawn_spec N (λ _, refines_right k (fill K #()))%I with "[He1 Hk]").
+ - wp_pures. wp_bind e1.
+ rewrite refines_eq /refines_def.
+ iAssert (spec_ctx) with "[Hk]" as "#Hs".
+ { iDestruct "Hk" as "[$ _]". }
+ iMod ("He1" with "Hk") as "He1".
+ iApply (wp_wand with "He1").
+ iIntros (?) "P". wp_pures.
+ rewrite /refines_right.
+ iDestruct "P" as (v') "[Hj [-> ->]]".
+ iFrame "Hs". by rewrite fill_app.
+ - iNext. iIntros (l) "Hl". simpl.
+ rel_pures_l. rel_bind_l e2.
+ iApply refines_wp_l.
+ iApply (wp_wand with "He2"). iIntros (?) "HQ".
+ simpl. rel_pures_l. rel_bind_l (spawn.join _).
+ iApply refines_wp_l.
+ wp_apply (join_spec with "Hl").
+ iIntros (?) "Hk".
+ iSpecialize ("Ht" with "HQ"). simpl.
+ rel_pures_l. iApply (refines_combine with "Ht Hk").
+ Qed.
(* Lemma par_r_1 e1 e2 t (A : lrel Σ) E : *)
(* ↑ relocN ⊆ E → *)
@@ -209,14 +212,17 @@ Section rules.
tp_pure i (App _ _). simpl.
rel_pures_r.
rel_bind_r e2.
- iApply refines_spec_ctx. iIntros "#Hs".
- iApply (par_l_1' (i ⤇ (#c2 <- InjR (#();; #())))%I
+ iApply (par_l_1' (refines_right i (#c2 <- InjR (#();; #())))%I
with "He2 [He1 Hi]").
{ rewrite refines_eq /refines_def.
tp_bind i e1.
- iMod ("He1" with "Hs Hi") as "He1". simpl.
+ rewrite refines_right_bind.
+ iAssert (spec_ctx) with "[Hi]" as "#Hs".
+ { iDestruct "Hi" as "[$ _]". }
+ iMod ("He1" with "Hi") as "He1". simpl.
iApply (wp_wand with "He1"). iIntros (?).
- iDestruct 1 as (?) "[Hi [-> ->]]". done. }
+ iDestruct 1 as (?) "[Hi [-> ->]]".
+ rewrite /refines_right. by iFrame. }
iIntros "Hi". simpl. rel_pures_r.
tp_pures i. tp_store i.
rel_rec_r. rel_load_r. rel_pures_r. rel_values.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 83aa92cb37df25a37eae8e9cb2acb70931b53336..ea03356da01c09a37c8eb435b4380554f73e6b00 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -47,7 +47,9 @@ Section refinement.
Lemma ticket_nondup γ n : ticket γ n -∗ ticket γ n -∗ False.
Proof.
iIntros "Ht1 Ht2".
- iDestruct (own_valid_2 with "Ht1 Ht2") as %?%gset_disj_valid_op.
+ iDestruct (own_valid_2 with "Ht1 Ht2") as %Hfoo.
+ revert Hfoo. rewrite -auth_frag_op auth_frag_valid.
+ intros ?%gset_disj_valid_op.
set_solver.
Qed.
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 7bfcd55db7a8ead3f60b6fc9f1f48561b704a879..9ff73d87a4120a19ae5869596146fb0919fd1c4d 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -232,7 +232,7 @@ Section proofs.
iDestruct "Hx'" as "[Hx' Hx'1]".
iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | Hbb]".
{ iCombine "Hx Hx1" as "Hx".
- iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
+ iDestruct (mapsto_valid_2 with "Hx Hx2") as %[Hfoo _]. exfalso.
compute in Hfoo. eauto. }
iMod ("Hcl" with "[Hx Hx' Hbb]") as "_".
{ iNext. iExists (S n).
@@ -244,7 +244,7 @@ Section proofs.
iDestruct (mapsto_agree with "Hx Hx1") as %->.
iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | (Hb & Hb')]".
{ iCombine "Hx Hx1" as "Hx".
- iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
+ iDestruct (mapsto_valid_2 with "Hx Hx2") as %[Hfoo _]. exfalso.
compute in Hfoo. eauto. }
iModIntro; iExists _; iFrame; iNext. iIntros "Hb".
rel_store_r.
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index bc33ecc2f18dbde56269cb526bff9f5f00dd18b7..1e4053a74ee1ea95a37955547aacb26096549b0d 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -83,12 +83,6 @@ Definition CG_mkstack : val := λ: <>,
value that is being offered and a potential thread with the
continuation that accepts the offer, if it is present. *)
-Canonical Structure ectx_itemO := leibnizO ectx_item.
-(* TODO: move !! *)
-Canonical Structure ref_idO := leibnizO ref_id.
-Global Instance ref_id_inhabited : Inhabited ref_id.
-Proof. split. apply (RefId 0 []). Qed.
-
Definition offerReg := gmap loc (val * gname * ref_id).
Definition offerRegR :=
gmapUR loc (agreeR (prodO valO (prodO gnameO ref_idO))).
diff --git a/theories/experimental/helping/offers.v b/theories/experimental/helping/offers.v
index 2bb656743ce858876c2b27857fcb89dc58a5a566..a3ffc5b1f9cb0479575e63ea39a91ed31e953989 100644
--- a/theories/experimental/helping/offers.v
+++ b/theories/experimental/helping/offers.v
@@ -37,7 +37,7 @@ Section rules.
is_offer γ1 l P1 Q1 -∗ is_offer γ2 l P2 Q2 -∗ False.
Proof.
iDestruct 1 as (?) "[Hl1 _]". iDestruct 1 as (?) "[Hl2 _]".
- iDestruct (gen_heap.mapsto_valid_2 with "Hl1 Hl2") as %?. contradiction.
+ iDestruct (gen_heap.mapsto_valid_2 with "Hl1 Hl2") as %[? _]. contradiction.
Qed.
Lemma make_is_offer γ l P Q : l ↦ #0 -∗ P -∗ is_offer γ l P Q.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 32343622ddeb6f665f5dd204f7f2a6c72bec5e30..a30b7baa0314fbea47f45d53be2aeb22ddfe1f9c 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -53,6 +53,16 @@ End lrel_ofe.
Arguments lrelC : clear implicits.
+Record ref_id := RefId {
+ tp_id : nat;
+ tp_ctx : list ectx_item }.
+
+Canonical Structure ectx_itemO := leibnizO ectx_item.
+Canonical Structure ref_idO := leibnizO ref_id.
+
+Global Instance ref_id_inhabited : Inhabited ref_id.
+Proof. split. apply (RefId 0 []). Qed.
+
Section semtypes.
Context `{relocG Σ}.
@@ -60,10 +70,6 @@ Section semtypes.
Implicit Types E : coPset.
Implicit Types A B : lrel Σ.
- Record ref_id := RefId {
- tp_id : nat;
- tp_ctx : list ectx_item }.
-
Definition rhs_t := sum expr ref_id.
Definition in_1 : expr -> rhs_t := inl.
Definition in_2 : ref_id -> rhs_t := inr.
@@ -187,7 +193,7 @@ Section semtypes_properties.
iInv (relocN.@"ref".@(l, l1')) as (? ?) "[>Hl ?]" "Hcl".
iInv (relocN.@"ref".@(l, l2')) as (? ?) "[>Hl' ?]" "Hcl'".
simpl. iExFalso.
- iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %Hfoo.
+ iDestruct (gen_heap.mapsto_valid_2 with "Hl Hl'") as %[Hfoo _].
compute in Hfoo. eauto.
Qed.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 5e76800d9dec7cb3c723b617e1383fce33936e5c..b0598f6be1b96c99c86eb8d5ed2f84ab36dc71f4 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -168,7 +168,8 @@ Section mapsto.
rewrite heapS_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
f_equiv=> /=.
rewrite -pair_op singleton_op right_id -pair_op.
- move=> [_ Hv]. move:Hv => /=.
+ rewrite auth_frag_valid pair_valid.
+ intros [_ Hv]. move:Hv => /=.
rewrite singleton_valid.
by move=> [_] /to_agree_op_inv_L [->].
Qed.
diff --git a/theories/prelude/asubst.v b/theories/prelude/asubst.v
index 64dccb032c2e126ce8ed338dc9d16ea576c82ade..c64cd5bbaca94618696818171147741711232e0a 100644
--- a/theories/prelude/asubst.v
+++ b/theories/prelude/asubst.v
@@ -1,6 +1,6 @@
(** Autosubst helper lemmata *)
From Autosubst Require Export Autosubst.
-From iris.algebra Require Export base.
+From iris.prelude Require Export prelude.
Section Autosubst_Lemmas.
Context {term : Type} {Ids_term : Ids term}