diff --git a/coq-reloc.opam b/coq-reloc.opam
index 392312ef3985c7a22ec5ac3ba9a8bf2716a54fdd..4dd23f35be999ec51af59f9f314b79c26db4d3d4 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-09-29.0.4f3a385f") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-11-06.5.4cfd3db8") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
index fe1fd29fc30cf732d16212c050c87bb5cedcc5c6..85425e40b2843fd972ff7d4d2f3e73428c93d8b1 100644
--- a/theories/examples/folly_queue/refinement.v
+++ b/theories/examples/folly_queue/refinement.v
@@ -94,7 +94,7 @@ Section queue_refinement.
 
   Definition ghost_list γl (xs : list val) := own γl (● make_map (list_idx_to_map xs)).
 
-  Definition ghost_list_mapsto γl i (x : val) := own γl (◯ {[i := to_agree x]}).
+  Definition ghost_list_pointsto γl i (x : val) := own γl (◯ {[i := to_agree x]}).
 
   Lemma ghost_list_alloc : ⊢ |==> ∃ γl, ghost_list γl [].
     iMod (own_alloc (● ∅ : listUR)) as (γl) "Hauth"; first by apply auth_auth_valid.
@@ -103,10 +103,10 @@ Section queue_refinement.
   Qed.
 
   Lemma ghost_list_append γl xs (x : val) :
-    ghost_list γl xs ==∗ ghost_list γl (xs ++ [x]) ∗ ghost_list_mapsto γl (length xs) x.
+    ghost_list γl xs ==∗ ghost_list γl (xs ++ [x]) ∗ ghost_list_pointsto γl (length xs) x.
   Proof.
     iIntros "HL".
-    rewrite /ghost_list /ghost_list_mapsto.
+    rewrite /ghost_list /ghost_list_pointsto.
     rewrite -(own_op γl).
     iApply (own_update with "HL").
     apply auth_update_alloc.
@@ -130,9 +130,9 @@ Section queue_refinement.
   Qed.
 
   Lemma ghost_list_le γl xs i x :
-    ghost_list γl xs -∗ ghost_list_mapsto γl i x -∗ ⌜i < length xs⌝.
+    ghost_list γl xs -∗ ghost_list_pointsto γl i x -∗ ⌜i < length xs⌝.
   Proof.
-    rewrite /ghost_list /ghost_list_mapsto /list_idx_to_map.
+    rewrite /ghost_list /ghost_list_pointsto /list_idx_to_map.
     iIntros "Ha Hb".
     iCombine "Ha Hb" gives %[Hincl _]%auth_both_valid_discrete.
     apply dom_included in Hincl.
@@ -146,10 +146,10 @@ Section queue_refinement.
 
   Lemma ghost_list_lookup (γl : gname) xs (i : nat) (x : val) :
     xs !! i = Some x →
-    ghost_list γl xs ==∗ ghost_list γl xs ∗ ghost_list_mapsto γl i x.
+    ghost_list γl xs ==∗ ghost_list γl xs ∗ ghost_list_pointsto γl i x.
   Proof.
     iIntros (Hs) "Hlist".
-    rewrite /ghost_list /ghost_list_mapsto /list_idx_to_map.
+    rewrite /ghost_list /ghost_list_pointsto /list_idx_to_map.
     rewrite -own_op.
     iApply (own_update with "Hlist").
     apply: auth_update_dfrac_alloc.
@@ -243,7 +243,7 @@ Section queue_refinement.
      we're at at the queue in total (global index n). *)
   Definition R γl q i (j : nat) (v : val) : iProp Σ :=
     let n := j * q + i
-    in ghost_list_mapsto γl n v.
+    in ghost_list_pointsto γl n v.
 
   (* Turn management. *)
 
@@ -575,7 +575,7 @@ Section queue_refinement.
     (∃ id v vₛ, own γm (◯ {[ i := to_agree id ]}) ∗
                 (refines_right id (of_val vₛ)) ∗
                 A v vₛ ∗
-                ghost_list_mapsto γl i v).
+                ghost_list_pointsto γl i v).
 
   Definition mpmcInv A γt γm γl q (ℓpop ℓpush ℓarr : loc) (SEQs : list seq)
     (xsᵢ : list val) (ℓs : loc) (lk : val) : iProp Σ :=
diff --git a/theories/examples/folly_queue/turnSequencer.v b/theories/examples/folly_queue/turnSequencer.v
index aa8aa44f8119a39a65a5e4d0ff4210e84e71ad1b..1cff42b6285f7855c2c3cd4d2da33b90fff2439a 100644
--- a/theories/examples/folly_queue/turnSequencer.v
+++ b/theories/examples/folly_queue/turnSequencer.v
@@ -125,7 +125,7 @@ Section spec.
       iCombine "â„“Pts Hc" gives %[?%Qp.not_add_le_l _].
       done. }
     wp_load.
-    iDestruct (mapsto_agree with "â„“Pts Hc") as %[= Heq].
+    iDestruct (pointsto_agree with "â„“Pts Hc") as %[= Heq].
     iMod ("Hcl" with "[Ht â„“Pts Hturns]") as "_".
     { iNext. iExists m. iFrame. }
     iModIntro. wp_pures. simplify_eq/=.
@@ -138,7 +138,7 @@ Section spec.
       iCombine "â„“Pts Hc'" as "â„“Pts".
       iCombine "â„“Pts Hc" gives %[?%Qp.not_add_le_l _].
       done. }
-    iDestruct (mapsto_combine with "â„“Pts Hc") as "[â„“Pts %Heq]".
+    iDestruct (pointsto_combine with "â„“Pts Hc") as "[â„“Pts %Heq]".
     simplify_eq/=.
     rewrite dfrac_op_own Qp.half_half.
     wp_store.
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index f0dd49e500ce1fe6ff10351449d293549127d4ae..e98b244233c1be962082d827ba8de113f9e77b7f 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -30,15 +30,15 @@ Section proof.
     - iIntros "#Histk".
       destruct ls' as [|h' ls']; first by eauto.
       simpl. iDestruct 1 as (z) "[Histk' _]".
-      iDestruct (mapsto_agree with "Histk' Histk") as %Hfoo.
+      iDestruct (pointsto_agree with "Histk' Histk") as %Hfoo.
       exfalso. naive_solver.
     - iDestruct 1 as (z) "[Histk Hls]".
       destruct ls' as [|h' ls']; simpl.
       + iIntros "Histk'".
-        iDestruct (mapsto_agree with "Histk' Histk") as %Hfoo.
+        iDestruct (pointsto_agree with "Histk' Histk") as %Hfoo.
         exfalso. naive_solver.
       + iDestruct 1 as (z') "[Histk' Hls']".
-        iDestruct (mapsto_agree with "Histk' Histk") as %Hfoo; simplify_eq/=.
+        iDestruct (pointsto_agree with "Histk' Histk") as %Hfoo; simplify_eq/=.
         iDestruct (IHls with "Hls Hls'") as %Hbar. simplify_eq/=.
         eauto.
   Qed.
@@ -76,7 +76,7 @@ Section proof.
       rel_pures_l. rel_rec_l. by iApply "IH".
     - (* CmpXchg succeeds *)
       iIntros (?). simplify_eq/=. iNext. iIntros "Hstk".
-      iMod (mapsto_persist with "Hnstk") as "Hnstk".
+      iMod (pointsto_persist with "Hnstk") as "Hnstk".
       rewrite /stack_link. iDestruct "Hlnk" as (ls1 ls2) "(Hls1 & Hls2 & #HA)".
       rel_apply_r (refines_CG_push_r with "Hls2").
       iIntros "Hls2".
@@ -157,7 +157,7 @@ Section proof.
       rel_alloc_r st' as "Hst'". rel_pures_r.
       rel_apply_r refines_newlock_r. iIntros (l) "Hl". rel_pures_r.
       rel_values.
-      iMod (mapsto_persist with "Hisk") as "#Hisk".
+      iMod (pointsto_persist with "Hisk") as "#Hisk".
       iMod (inv_alloc (stackN.@(st,(#st', l)%V)) _ (sinv A st (#st', l)%V) with "[-]")
         as "#Hinv".
       { iNext. iExists _. iFrame. iExists [],[]. simpl.
diff --git a/theories/examples/stack_helping/helping_wrapper.v b/theories/examples/stack_helping/helping_wrapper.v
index 892bbd87c6b359f2e5125708f7ffaed5ac3ed9bd..ac20b43e873b74ed6882824e7c3ac004b86cfa59 100644
--- a/theories/examples/stack_helping/helping_wrapper.v
+++ b/theories/examples/stack_helping/helping_wrapper.v
@@ -422,7 +422,7 @@ Section stack_example.
     destruct ls1 as [|h1 ls1]; simpl; rel_rec_l; rel_pures_l.
     - iInv stackN as (ls1 ls2) "(>Hst1 & >Hst2 & HA)" "Hcl".
       iDestruct "Hst2" as (st2l lk2 ->) "[Hlk Hst2]".
-      iDestruct (mapsto_agree with "Hl1 Hst1") as %Hfoo.
+      iDestruct (pointsto_agree with "Hl1 Hst1") as %Hfoo.
       assert (ls1 = []) as ->.
       { revert Hfoo; by destruct ls1. }
       rel_rec_r. rel_pures_r. rel_apply_r (refines_acquire_r with "Hlk").
@@ -441,7 +441,7 @@ Section stack_example.
     - rel_store_l_atomic.
       iInv stackN as (ls1' ls2) "(>Hst1 & >Hst2 & HA)" "Hcl".
       iDestruct "Hst2" as (st2l lk2 ->) "[Hlk Hst2]".
-      iDestruct (mapsto_agree with "Hl1 Hst1") as %Hfoo.
+      iDestruct (pointsto_agree with "Hl1 Hst1") as %Hfoo.
       assert (ls1' = h1::ls1) as ->.
       { destruct ls1'; simplify_eq/=; eauto. }
       iModIntro. iExists _. iFrame. iNext. iIntros "Hl1".
@@ -481,7 +481,7 @@ Section stack_example.
     rel_store_l_atomic.
     iInv stackN as (ls1' ls2) "(>Hst1 & >Hst2 & HA)" "Hcl".
     iDestruct "Hst2" as (st2l lk2 ->) "[Hlk Hst2]".
-    iDestruct (mapsto_agree with "Hl1 Hst1") as %Hfoo. simplify_eq/=.
+    iDestruct (pointsto_agree with "Hl1 Hst1") as %Hfoo. simplify_eq/=.
     iModIntro. iExists _. iFrame. iNext. iIntros "Hl1".
     rel_rec_r. rel_pures_r. rel_apply_r (refines_acquire_r with "Hlk").
     iIntros "Hlk". rel_pures_r. rel_rec_r. rel_load_r.
diff --git a/theories/examples/stack_helping/stack.v b/theories/examples/stack_helping/stack.v
index 72fe38524145498be9557a834da6711fb9547074..2bbfab190a50ff88a6974e56047ab2920e235162 100644
--- a/theories/examples/stack_helping/stack.v
+++ b/theories/examples/stack_helping/stack.v
@@ -308,7 +308,7 @@ Section refinement.
       iDestruct 1 as (z) "[Histk Hls]".
       destruct ls' as [|h' ls']; simpl; eauto.
       iDestruct 1 as (z') "[Histk' Hls']".
-      iDestruct (mapsto_agree with "Histk' Histk") as %Hfoo. simplify_eq/=.
+      iDestruct (pointsto_agree with "Histk' Histk") as %Hfoo. simplify_eq/=.
       iDestruct (IHls with "Hls Hls'") as %Hbar. simplify_eq/=.
       eauto.
   Qed.
@@ -533,7 +533,7 @@ Section refinement.
         iIntros "Hol".
         rel_apply_r (refines_CG_push_r with "Hst2").
         iIntros "Hst2".
-        iMod (mapsto_persist with "Hnew") as "#Hnew".
+        iMod (pointsto_persist with "Hnew") as "#Hnew".
         iMod ("Hcl" with "[-]") as "_".
         { iNext. iExists (Some new),_,(h1::ls1'),_; iFrame.
           simpl. by eauto with iFrame. }
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 5b58aadb8499e790782b5dbae25e9cf27e8ebdb3..2adb37bad2e9ea51aee4fb4d84f4118192acbf5a 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -250,10 +250,10 @@ Section proof.
       rel_load_l. repeat rel_pure_l.
       rel_store_l_atomic.
       iInv sizeN as (m' ls') "(Ha & >Hs1' & >Hs2' & >Htbl1' & >Htbl2' & #Hls)" "Hcl".
-      iDestruct (mapsto_agree with "Hs1 Hs1'") as %Hm'.
+      iDestruct (pointsto_agree with "Hs1 Hs1'") as %Hm'.
       simplify_eq/=.
       iCombine "Hs1 Hs1'" as "Hs1".
-      iDestruct (mapsto_agree with "Htbl1 Htbl1'") as %->.
+      iDestruct (pointsto_agree with "Htbl1 Htbl1'") as %->.
       iModIntro. iExists _. iFrame. iNext. iIntros "[Hs1 Hs1']".
       repeat rel_pure_l.
       rel_apply_r (refines_acquire_r with "Hl2").
@@ -273,7 +273,7 @@ Section proof.
       rel_store_l_atomic.
       iClear "Hls".
       iInv sizeN as (m ls) "(Ha & >Hs1 & >Hs2 & >Htbl1 & >Htbl2 & #Hls)" "Hcl".
-      iDestruct (gen_heap.mapsto_agree with "Htbl1 Htbl1'") as %->.
+      iDestruct (gen_heap.pointsto_agree with "Htbl1 Htbl1'") as %->.
       iCombine "Htbl1 Htbl1'" as "Htbl1".
       iModIntro. iExists _. iFrame. iNext. iIntros "[Htbl1 Htbl1']".
       repeat rel_pure_l. repeat rel_pure_r. rel_load_r.
@@ -329,10 +329,10 @@ Section proof.
       rel_load_l. repeat rel_pure_l.
       rel_store_l_atomic.
       iInv sizeN as (m' ls') "(Ha & >Hs1' & >Hs2' & >Htbl1' & >Htbl2' & #Hls)" "Hcl".
-      iDestruct (mapsto_agree with "Hs1 Hs1'") as %Hm'.
+      iDestruct (pointsto_agree with "Hs1 Hs1'") as %Hm'.
       simplify_eq/=.
       iCombine "Hs1 Hs1'" as "Hs1".
-      iDestruct (mapsto_agree with "Htbl1 Htbl1'") as %->.
+      iDestruct (pointsto_agree with "Htbl1 Htbl1'") as %->.
       iModIntro. iExists _. iFrame. iNext. iIntros "[Hs1 Hs1']".
       repeat rel_pure_l.
       rel_apply_r (refines_acquire_r with "Hl2").
@@ -352,7 +352,7 @@ Section proof.
       rel_store_l_atomic.
       iClear "Hls".
       iInv sizeN as (m ls) "(Ha & >Hs1 & >Hs2 & >Htbl1 & >Htbl2 & #Hls)" "Hcl".
-      iDestruct (mapsto_agree with "Htbl1 Htbl1'") as %->.
+      iDestruct (pointsto_agree with "Htbl1 Htbl1'") as %->.
       iCombine "Htbl1 Htbl1'" as "Htbl1".
       iModIntro. iExists _. iFrame. iNext. iIntros "[Htbl1 Htbl1']".
       repeat rel_pure_l. repeat rel_pure_r. rel_load_r.
diff --git a/theories/examples/various.v b/theories/examples/various.v
index a1737c3655a617fd292c3f18616a84f7d1b4602b..07a6d848c8c39222cd358892afd80ae9c8c1cc38 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -220,7 +220,7 @@ Section proofs.
         rel_load_l. rel_pure_l. rel_pure_r.
         rel_store_l_atomic.
         iInv i3n as (n') "(>Hx & Hx' & >Hbb)" "Hcl".
-        iDestruct (mapsto_agree with "Hx Hx1") as %->.
+        iDestruct (pointsto_agree with "Hx Hx1") as %->.
         iCombine "Hx Hx1" as "Hx".
         iModIntro. iExists _; iFrame. iNext.
         iIntros "Hx".
@@ -239,7 +239,7 @@ Section proofs.
         repeat rel_pure_l. repeat rel_pure_r.
         rel_store_l_atomic. clear n'.
         iInv i3n as (n') "(>Hx & Hx' & >Hbb)" "Hcl".
-        iDestruct (mapsto_agree with "Hx Hx1") as %->.
+        iDestruct (pointsto_agree with "Hx Hx1") as %->.
         iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | (Hb & Hb')]".
         { iCombine "Hx Hx1" as "Hx".
           iCombine "Hx Hx2" gives %[Hfoo _]. exfalso.
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index c05ba0d8a657f42dc13233d12dc95034b281f4d8..b0fb3424c616a9d65173739923aeab7badfdd75b 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -42,7 +42,7 @@ Proof.
     iApply fupd_wp. iApply ("Hrel" $! (RefId 0 [])).
     iSplitR.
     + iExists _. by iFrame.
-    + rewrite tpool_mapsto_eq /tpool_mapsto_def.
+    + rewrite tpool_pointsto_eq /tpool_pointsto_def.
       by rewrite /to_tpool /= insert_empty map_fmap_singleton //.
   - iIntros (v).
     iDestruct 1 as (v') "[Hj Hinterp]".
@@ -50,7 +50,7 @@ Proof.
     iDestruct "Hinterp" as %Hinterp.
     iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
     iDestruct "Hj" as "[#Hs Hj]".
-    rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
+    rewrite tpool_pointsto_eq /tpool_pointsto_def /=.
     iCombine "Hown Hj" gives %Hvalid.
     move: Hvalid=> /auth_both_valid_discrete
        [/prod_included [/tpool_singleton_included Hv2 _] _].
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index de6e53fbd8ae1e0fa4c6c1d1935a930f5afe1767..8681a9055aea7b76570780ac1922a8500ac8b6a5 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -233,7 +233,7 @@ Proof.
 Qed.
 
 Tactic Notation "rel_load_l" :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
     iAssumptionCore || fail "rel_load_l: cannot find" l "↦ ?" in
   rel_pures_l;
@@ -243,7 +243,7 @@ Tactic Notation "rel_load_l" :=
     |fail 1 "rel_load_l: cannot find 'Load'"];
   (* the remaining goals are from tac_lel_load_l (except for the first one, which has already been solved by this point) *)
   [tc_solve             (** IntoLaters *)
-  |solve_mapsto ()
+  |solve_pointsto ()
   |reflexivity       (** eres = fill K v *)
   |rel_finish  (** new goal *)].
 
@@ -255,7 +255,7 @@ errors in a more precise way. E.g. if we are executing !#l and l ↦ₛ is
 not found in the environment, then we can immediately fail with an
 error *)
 Tactic Notation "rel_load_r" :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦ₛ{_} _)%I) => l end in
     iAssumptionCore || fail "rel_load_r: cannot find" l "↦ₛ ?" in
   rel_pures_r;
@@ -265,7 +265,7 @@ Tactic Notation "rel_load_r" :=
     |fail 1 "rel_load_r: cannot find 'Load'"];
   (* the remaining goals are from tac_rel_load_r (except for the first one, which has already been solved by this point) *)
   [solve_ndisj || fail "rel_load_r: cannot prove 'nclose specN ⊆ ?'"
-  |solve_mapsto ()
+  |solve_pointsto ()
   |reflexivity
   |rel_finish  (** new goal *)].
 
@@ -311,7 +311,7 @@ Proof.
 Qed.
 
 Tactic Notation "rel_store_l" :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦ _)%I) => l end in
     iAssumptionCore || fail "rel_store_l: cannot find" l "↦ₛ ?" in
   rel_pures_l;
@@ -324,7 +324,7 @@ Tactic Notation "rel_store_l" :=
     |fail 1 "rel_store_l: cannot find 'Store'"];
   (* the remaining goals are from tac_rel_store_l (except for the first one, which has already been solved by this point) *)
   [tc_solve        (** IntoLaters *)
-  |solve_mapsto ()
+  |solve_pointsto ()
   |pm_reflexivity || fail "rel_store_l: this should not happen O-:"
   |reflexivity
   |rel_finish  (** new goal *)].
@@ -332,7 +332,7 @@ Tactic Notation "rel_store_l" :=
 Tactic Notation "rel_store_l_atomic" := rel_apply_l refines_store_l.
 
 Tactic Notation "rel_store_r" :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦ₛ _)%I) => l end in
     iAssumptionCore || fail "rel_store_r: cannot find" l "↦ₛ ?" in
   rel_pures_r;
@@ -343,7 +343,7 @@ Tactic Notation "rel_store_r" :=
     |fail 1 "rel_store_r: cannot find 'Store'"];
   (* the remaining goals are from tac_rel_store_r (except for the first one, which has already been solved by this point) *)
   [solve_ndisj || fail "rel_store_r: cannot prove 'nclose specN ⊆ ?'"
-  |solve_mapsto ()
+  |solve_pointsto ()
   |pm_reflexivity || fail "rel_store_r: this should not happen O-:"
   |reflexivity
   |rel_finish  (** new goal *)].
@@ -390,7 +390,7 @@ Proof.
 Qed.
 
 Tactic Notation "rel_xchg_l" :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦ _)%I) => l end in
     iAssumptionCore || fail "rel_xchg_l: cannot find" l "↦ₛ ?" in
   rel_pures_l;
@@ -403,7 +403,7 @@ Tactic Notation "rel_xchg_l" :=
     |fail 1 "rel_xchg_l: cannot find 'Xchg'"];
   (* the remaining goals are from tac_rel_xchg_l (except for the first one, which has already been solved by this point) *)
   [tc_solve        (** IntoLaters *)
-  |solve_mapsto ()
+  |solve_pointsto ()
   |pm_reflexivity || fail "rel_xchg_l: this should not happen O-:"
   |reflexivity
   |rel_finish  (** new goal *)].
@@ -411,7 +411,7 @@ Tactic Notation "rel_xchg_l" :=
 Tactic Notation "rel_xchg_l_atomic" := rel_apply_l refines_xchg_l.
 
 Tactic Notation "rel_xchg_r" :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦ₛ _)%I) => l end in
     iAssumptionCore || fail "rel_xchg_r: cannot find" l "↦ₛ ?" in
   rel_pures_r;
@@ -422,7 +422,7 @@ Tactic Notation "rel_xchg_r" :=
     |fail 1 "rel_xchg_r: cannot find 'Xchg'"];
   (* the remaining goals are from tac_rel_xchg_r (except for the first one, which has already been solved by this point) *)
   [solve_ndisj || fail "rel_xchg_r: cannot prove 'nclose specN ⊆ ?'"
-  |solve_mapsto ()
+  |solve_pointsto ()
   |pm_reflexivity || fail "rel_xchg_r: this should not happen O-:"
   |reflexivity
   |rel_finish  (** new goal *)].
@@ -536,7 +536,7 @@ Proof.
 Qed.
 
 Tactic Notation "rel_cmpxchg_fail_r" :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦ₛ _)%I) => l end in
     iAssumptionCore || fail "rel_cmpxchg_fail_r: cannot find" l "↦ₛ ?" in
   rel_pures_r;
@@ -550,14 +550,14 @@ Tactic Notation "rel_cmpxchg_fail_r" :=
     |fail 1 "rel_cmpxchg_fail_r: cannot find 'CmpXchg'"];
   (* the remaining goals are from tac_rel_cmpxchg_fail_r (except for the first one, which has already been solved by this point) *)
   [solve_ndisj || fail "rel_cmpxchg_fail_r: cannot prove 'nclose specN ⊆ ?'"
-  |solve_mapsto ()
+  |solve_pointsto ()
   |try (simpl; congruence)   (** v ≠ v1 *)
   |try heap_lang.proofmode.solve_vals_compare_safe
   |reflexivity
   |rel_finish  (** new goal *)].
 
 Tactic Notation "rel_cmpxchg_suc_r" :=
-  let solve_mapsto _ :=
+  let solve_pointsto _ :=
     let l := match goal with |- _ = Some (_, (?l ↦ₛ _)%I) => l end in
     iAssumptionCore || fail "rel_cmpxchg_suc_r: cannot find" l "↦ₛ ?" in
   rel_pures_r;
@@ -571,7 +571,7 @@ Tactic Notation "rel_cmpxchg_suc_r" :=
     |fail 1 "rel_cmpxchg_suc_r: cannot find 'CmpXchg'"];
   (* the remaining goals are from tac_rel_cmpxchg_suc_r (except for the first one, which has already been solved by this point) *)
   [solve_ndisj || fail "rel_cmpxchg_suc_r: cannot prove 'nclose specN ⊆ ?'"
-  |solve_mapsto ()
+  |solve_pointsto ()
   |try (simpl; congruence)   (** v = v1 *)
   |try heap_lang.proofmode.solve_vals_compare_safe
   |pm_reflexivity  (** new env *)
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 790f4d3c51cf15ea59d7655e1dc31dd1049ec00a..5f27f2f9045c5ec2df7b77536faa2cef2c43f8c5 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -30,19 +30,19 @@ Definition to_tpool (tp : list expr) : tpoolUR := Excl <$> (map_seq 0 tp).
 Section definitionsS.
   Context `{cfgSG Σ, invGS Σ}.
 
-  Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
+  Definition heapS_pointsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
     own cfg_name (◯ (∅, {[ l := (q, to_agree (Some v)) ]})).
-  Definition heapS_mapsto_aux : seal (@heapS_mapsto_def). by eexists. Qed.
-  Definition heapS_mapsto := heapS_mapsto_aux.(unseal).
-  Definition heapS_mapsto_eq :
-    @heapS_mapsto = @heapS_mapsto_def := heapS_mapsto_aux.(seal_eq).
+  Definition heapS_pointsto_aux : seal (@heapS_pointsto_def). by eexists. Qed.
+  Definition heapS_pointsto := heapS_pointsto_aux.(unseal).
+  Definition heapS_pointsto_eq :
+    @heapS_pointsto = @heapS_pointsto_def := heapS_pointsto_aux.(seal_eq).
 
-  Definition tpool_mapsto_def (j : nat) (e: expr) : iProp Σ :=
+  Definition tpool_pointsto_def (j : nat) (e: expr) : iProp Σ :=
     own cfg_name (◯ ({[ j := Excl e ]}, ∅)).
-  Definition tpool_mapsto_aux : seal (@tpool_mapsto_def). by eexists. Qed.
-  Definition tpool_mapsto := tpool_mapsto_aux.(unseal).
-  Definition tpool_mapsto_eq :
-    @tpool_mapsto = @tpool_mapsto_def := tpool_mapsto_aux.(seal_eq).
+  Definition tpool_pointsto_aux : seal (@tpool_pointsto_def). by eexists. Qed.
+  Definition tpool_pointsto := tpool_pointsto_aux.(unseal).
+  Definition tpool_pointsto_eq :
+    @tpool_pointsto = @tpool_pointsto_def := tpool_pointsto_aux.(seal_eq).
 
   Definition mkstate (σ : gmap loc (option val)) (κs : gset proph_id) :=
     {| heap := σ; used_proph_id := κs |}.
@@ -52,18 +52,18 @@ Section definitionsS.
   Definition spec_ctx : iProp Σ :=
     (∃ ρ, inv specN (spec_inv ρ))%I.
 
-  Global Instance heapS_mapsto_timeless l q v : Timeless (heapS_mapsto l q v).
-  Proof. rewrite heapS_mapsto_eq. apply _. Qed.
-  Global Instance tpool_mapsto_timeless j e: Timeless (tpool_mapsto j e).
-  Proof. rewrite tpool_mapsto_eq. apply _. Qed.
+  Global Instance heapS_pointsto_timeless l q v : Timeless (heapS_pointsto l q v).
+  Proof. rewrite heapS_pointsto_eq. apply _. Qed.
+  Global Instance tpool_pointsto_timeless j e: Timeless (tpool_pointsto j e).
+  Proof. rewrite tpool_pointsto_eq. apply _. Qed.
   Global Instance spec_ctx_persistent : Persistent spec_ctx.
   Proof. apply _. Qed.
 End definitionsS.
 
-Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v)
+Notation "l ↦ₛ{ q } v" := (heapS_pointsto l q v)
   (at level 20, q at level 50, format "l  ↦ₛ{ q }  v") : bi_scope.
-Notation "l ↦ₛ v" := (heapS_mapsto l 1 v) (at level 20) : bi_scope.
-Notation "j ⤇ e" := (tpool_mapsto j e) (at level 20) : bi_scope.
+Notation "l ↦ₛ v" := (heapS_pointsto l 1 v) (at level 20) : bi_scope.
+Notation "j ⤇ e" := (tpool_pointsto j e) (at level 20) : bi_scope.
 
 Section conversions.
   Context `{cfgSG Σ}.
@@ -148,12 +148,12 @@ Section to_heap.
 
 End to_heap.
 
-Section mapsto.
+Section pointsto.
   Context `{!cfgSG Σ}.
 
   Global Instance mapstoS_fractional l v : Fractional (λ q, l ↦ₛ{q} v)%I.
   Proof.
-    intros p q. rewrite heapS_mapsto_eq -own_op -auth_frag_op.
+    intros p q. rewrite heapS_pointsto_eq -own_op -auth_frag_op.
     by rewrite -pair_op singleton_op -pair_op agree_idemp right_id.
   Qed.
   Global Instance mapstoS_as_fractional l q v :
@@ -167,7 +167,7 @@ Section mapsto.
   Lemma mapstoS_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
     apply bi.entails_wand, bi.wand_intro_r.
-    rewrite heapS_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
+    rewrite heapS_pointsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
     f_equiv=> /=.
     rewrite -pair_op singleton_op right_id -pair_op.
     rewrite auth_frag_valid pair_valid.
@@ -178,7 +178,7 @@ Section mapsto.
 
   Lemma mapstoS_valid l q v : l ↦ₛ{q} v -∗ ✓ q.
   Proof.
-    rewrite heapS_mapsto_eq /heapS_mapsto_def own_valid !uPred.discrete_valid.
+    rewrite heapS_pointsto_eq /heapS_pointsto_def own_valid !uPred.discrete_valid.
     apply bi.entails_wand, pure_mono=> /auth_frag_valid /= [_ Hfoo].
     revert Hfoo. simpl. rewrite singleton_valid.
     by intros [? _].
@@ -206,4 +206,4 @@ Section mapsto.
     iSplit; eauto. iCombine "Hl1 Hl2" as "?". done.
   Qed.
 
-End mapsto.
+End pointsto.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 95a6751b790a86d094c172427a73be2efd66fe4b..da703eb0148ae1bd76dc3e02055ba38cdbf30ad0 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -25,7 +25,7 @@ Section rules.
 
   (** * Aux. lemmas *)
   Lemma step_insert K tp j e σ κ e' σ' efs :
-    tp !! j = Some (fill K e) → head_step e σ κ e' σ' efs →
+    tp !! j = Some (fill K e) → base_step e σ κ e' σ' efs →
     erased_step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
   Proof.
     intros. rewrite -(take_drop_middle tp j (fill K e)) //.
@@ -36,7 +36,7 @@ Section rules.
   Qed.
 
   Lemma step_insert_no_fork K tp j e σ κ e' σ' :
-    tp !! j = Some (fill K e) → head_step e σ κ e' σ' [] →
+    tp !! j = Some (fill K e) → base_step e σ κ e' σ' [] →
     erased_step (tp, σ) (<[j:=fill K e']> tp, σ').
   Proof. rewrite -(right_id_L [] (++) (<[_:=_]>_)). by apply step_insert. Qed.
 
@@ -49,7 +49,7 @@ Section rules.
     spec_ctx ∗ j ⤇ fill K e ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K e'.
   Proof.
     iIntros (HP Hex ?) "[#Hspec Hj]". iFrame "Hspec".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
+    rewrite /spec_ctx tpool_pointsto_eq /tpool_pointsto_def /=.
     iDestruct "Hspec" as (ρ) "Hspec".
     iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose".
     iDestruct "Hrtc" as %Hrtc.
@@ -95,7 +95,7 @@ Section rules.
     ∃ (p : proph_id), spec_ctx ∗ j ⤇ fill K #p.
   Proof.
     iIntros (?) "[#Hinv Hj]". iFrame "Hinv".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
+    rewrite /spec_ctx tpool_pointsto_eq /tpool_pointsto_def /=.
     iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iCombine "Hown Hj"
@@ -116,7 +116,7 @@ Section rules.
     spec_ctx ∗ j ⤇ fill K #().
   Proof.
     iIntros (?) "[#Hinv Hj]". iFrame "Hinv".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
+    rewrite /spec_ctx tpool_pointsto_eq /tpool_pointsto_def /=.
     iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iCombine "Hown Hj"
@@ -137,7 +137,7 @@ Section rules.
     spec_ctx ∗ j ⤇ fill K (ref e) ⊢ |={E}=> ∃ l, spec_ctx ∗ j ⤇ fill K (#l) ∗ l ↦ₛ v.
   Proof.
     iIntros (<-?) "[#Hinv Hj]". iFrame "Hinv".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
+    rewrite /spec_ctx tpool_pointsto_eq /tpool_pointsto_def /=.
     iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     destruct (exist_fresh (dom (heap σ))) as [l Hl%not_elem_of_dom].
@@ -150,7 +150,7 @@ Section rules.
     { eapply auth_update_alloc, prod_local_update_2,
         (alloc_singleton_local_update _ l (1%Qp,to_agree (Some v : leibnizO _))); last done.
       by apply lookup_to_heap_None. }
-    rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
+    rewrite heapS_pointsto_eq /heapS_pointsto_def /=.
     iExists l. iFrame "Hj Hl". iApply "Hclose". iNext.
     iExists (<[j:=fill K (# l)]> tp), (state_upd_heap <[l:=Some v]> σ).
     rewrite to_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
@@ -165,9 +165,9 @@ Section rules.
     ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K (of_val v) ∗ l ↦ₛ{q} v.
   Proof.
     iIntros (?) "(#Hinv & Hj & Hl)". iFrame "Hinv".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
+    rewrite /spec_ctx tpool_pointsto_eq /tpool_pointsto_def.
     iDestruct "Hinv" as (ρ) "Hinv".
-    rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
+    rewrite heapS_pointsto_eq /heapS_pointsto_def /=.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iCombine "Hown Hj"
       gives %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
@@ -189,9 +189,9 @@ Section rules.
     ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K #() ∗ l ↦ₛ v.
   Proof.
     iIntros (<-?) "(#Hinv & Hj & Hl)". iFrame "Hinv".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
+    rewrite /spec_ctx tpool_pointsto_eq /tpool_pointsto_def.
     iDestruct "Hinv" as (ρ) "Hinv".
-    rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
+    rewrite heapS_pointsto_eq /heapS_pointsto_def /=.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iCombine "Hown Hj"
       gives %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
@@ -220,9 +220,9 @@ Section rules.
     ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K (of_val v') ∗ l ↦ₛ v.
   Proof.
     iIntros (<-?) "(#Hinv & Hj & Hl)". iFrame "Hinv".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
+    rewrite /spec_ctx tpool_pointsto_eq /tpool_pointsto_def.
     iDestruct "Hinv" as (ρ) "Hinv".
-    rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
+    rewrite heapS_pointsto_eq /heapS_pointsto_def /=.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iCombine "Hown Hj"
       gives %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
@@ -255,7 +255,7 @@ Section rules.
     ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K (v', #false)%V ∗ l ↦ₛ{q} v'.
   Proof.
     iIntros (<-<-???) "(#Hinv & Hj & Hl)". iFrame "Hinv".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
+    rewrite /spec_ctx tpool_pointsto_eq /tpool_pointsto_def heapS_pointsto_eq /heapS_pointsto_def.
     iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iCombine "Hown Hj"
@@ -282,7 +282,7 @@ Section rules.
     ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K (v1', #true)%V ∗ l ↦ₛ v2.
   Proof.
     iIntros (<-<-???) "(#Hinv & Hj & Hl)"; subst. iFrame "Hinv".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
+    rewrite /spec_ctx tpool_pointsto_eq /tpool_pointsto_def heapS_pointsto_eq /heapS_pointsto_def.
     iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iCombine "Hown Hj"
@@ -313,7 +313,7 @@ Section rules.
     ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K #i1 ∗ l ↦ₛ #(i1+i2).
   Proof.
     iIntros (<-?) "(#Hinv & Hj & Hl)"; subst. iFrame "Hinv".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
+    rewrite /spec_ctx tpool_pointsto_eq /tpool_pointsto_def heapS_pointsto_eq /heapS_pointsto_def.
     iDestruct "Hinv" as (ρ) "Hinv".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iCombine "Hown Hj"
@@ -343,7 +343,7 @@ Section rules.
     ∃ j', (spec_ctx ∗ j ⤇ fill K #()) ∗ (spec_ctx ∗ j' ⤇ e).
   Proof.
     iIntros (?) "[#Hspec Hj]". iFrame "Hspec".
-    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
+    rewrite /spec_ctx tpool_pointsto_eq /tpool_pointsto_def.
     iDestruct "Hspec" as (ρ) "Hspec".
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iCombine "Hown Hj"