From 4f0198fbd02189baa8f78356bcb4c0d54f786c0d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Apr 2016 23:43:23 +0200
Subject: [PATCH] Turn locations into literals.

This gets rid of the (ambiguous) notation %l, because we can declare
LitLoc as a coercion. It also shortens the code.
---
 heap_lang/heap.v                      | 10 +++++-----
 heap_lang/lang.v                      | 26 +++++++++-----------------
 heap_lang/lib/barrier/client.v        |  2 +-
 heap_lang/lib/barrier/proof.v         |  6 +++---
 heap_lang/lib/barrier/specification.v |  6 +++---
 heap_lang/lib/lock.v                  |  6 +++---
 heap_lang/lib/spawn.v                 |  4 ++--
 heap_lang/lifting.v                   | 12 ++++++------
 heap_lang/notation.v                  | 10 +++++-----
 heap_lang/proofmode.v                 | 17 +++++++++--------
 heap_lang/substitution.v              |  4 ----
 heap_lang/tactics.v                   |  1 -
 tests/joining_existentials.v          |  2 +-
 13 files changed, 47 insertions(+), 59 deletions(-)

diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 88e25dac6..39b5f441e 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -142,7 +142,7 @@ Section heap.
   Lemma wp_alloc N E e v P Φ :
     to_val e = Some v →
     P ⊢ heap_ctx N → nclose N ⊆ E →
-    P ⊢ (▷ ∀ l, l ↦ v -★ Φ (LocV l)) →
+    P ⊢ (▷ ∀ l, l ↦ v -★ Φ (LitV (LitLoc l))) →
     P ⊢ WP Alloc e @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv=> ??? HP.
@@ -168,7 +168,7 @@ Section heap.
   Lemma wp_load N E l q v P Φ :
     P ⊢ heap_ctx N → nclose N ⊆ E →
     P ⊢ (▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v)) →
-    P ⊢ WP Load (Loc l) @ E {{ Φ }}.
+    P ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv=> ?? HPΦ.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
@@ -185,7 +185,7 @@ Section heap.
     to_val e = Some v →
     P ⊢ heap_ctx N → nclose N ⊆ E →
     P ⊢ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))) →
-    P ⊢ WP Store (Loc l) e @ E {{ Φ }}.
+    P ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv=> ??? HPΦ.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
@@ -202,7 +202,7 @@ Section heap.
     to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 →
     P ⊢ heap_ctx N → nclose N ⊆ E →
     P ⊢ (▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false)))) →
-    P ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
+    P ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv=>????? HPΦ.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
@@ -219,7 +219,7 @@ Section heap.
     to_val e1 = Some v1 → to_val e2 = Some v2 →
     P ⊢ heap_ctx N → nclose N ⊆ E →
     P ⊢ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))) →
-    P ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
+    P ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv=> ???? HPΦ.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index b58ba23eb..153c1f3e2 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -9,7 +9,7 @@ Open Scope Z_scope.
 Definition loc := positive. (* Really, any countable type. *)
 
 Inductive base_lit : Set :=
-  | LitInt (n : Z) | LitBool (b : bool) | LitUnit.
+  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
 Inductive un_op : Set :=
   | NegOp | MinusUnOp.
 Inductive bin_op : Set :=
@@ -80,7 +80,6 @@ Inductive expr (X : list string) :=
   (* Concurrency *)
   | Fork (e : expr X)
   (* Heap *)
-  | Loc (l : loc)
   | Alloc (e : expr X)
   | Load (e : expr X)
   | Store (e1 : expr X) (e2 : expr X)
@@ -102,7 +101,6 @@ Arguments InjL {_} _%E.
 Arguments InjR {_} _%E.
 Arguments Case {_} _%E _%E _%E.
 Arguments Fork {_} _%E.
-Arguments Loc {_} _.
 Arguments Alloc {_} _%E.
 Arguments Load {_} _%E.
 Arguments Store {_} _%E _%E.
@@ -113,8 +111,7 @@ Inductive val :=
   | LitV (l : base_lit)
   | PairV (v1 v2 : val)
   | InjLV (v : val)
-  | InjRV (v : val)
-  | LocV (l : loc).
+  | InjRV (v : val).
 
 Bind Scope val_scope with val.
 Delimit Scope val_scope with V.
@@ -131,7 +128,6 @@ Fixpoint of_val (v : val) : expr [] :=
   | PairV v1 v2 => Pair (of_val v1) (of_val v2)
   | InjLV v => InjL (of_val v)
   | InjRV v => InjR (of_val v)
-  | LocV l => Loc l
   end.
 
 Fixpoint to_val (e : expr []) : option val :=
@@ -141,7 +137,6 @@ Fixpoint to_val (e : expr []) : option val :=
   | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
   | InjL e => InjLV <$> to_val e
   | InjR e => InjRV <$> to_val e
-  | Loc l => Some (LocV l)
   | _ => None
   end.
 
@@ -217,7 +212,6 @@ Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
   | InjR e => InjR (wexpr H e)
   | Case e0 e1 e2 => Case (wexpr H e0) (wexpr H e1) (wexpr H e2)
   | Fork e => Fork (wexpr H e)
-  | Loc l => Loc l
   | Alloc e => Alloc (wexpr H e)
   | Load  e => Load (wexpr H e)
   | Store e1 e2 => Store (wexpr H e1) (wexpr H e2)
@@ -260,7 +254,6 @@ Program Fixpoint wsubst {X Y} (x : string) (es : expr [])
   | Case e0 e1 e2 =>
      Case (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
   | Fork e => Fork (wsubst x es H e)
-  | Loc l => Loc l
   | Alloc e => Alloc (wsubst x es H e)
   | Load e => Load (wsubst x es H e)
   | Store e1 e2 => Store (wsubst x es H e1) (wsubst x es H e2)
@@ -322,21 +315,21 @@ Inductive head_step : expr [] → state → expr [] → state → option (expr [
      head_step (Fork e) σ (Lit LitUnit) σ (Some e)
   | AllocS e v σ l :
      to_val e = Some v → σ !! l = None →
-     head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
+     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) None
   | LoadS l v σ :
      σ !! l = Some v →
-     head_step (Load (Loc l)) σ (of_val v) σ None
+     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ None
   | StoreS l e v σ :
      to_val e = Some v → is_Some (σ !! l) →
-     head_step (Store (Loc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
+     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
   | CasFailS l e1 v1 e2 v2 vl σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some vl → vl ≠ v1 →
-     head_step (CAS (Loc l) e1 e2) σ (Lit $ LitBool false) σ None
+     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ None
   | CasSucS l e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some v1 →
-     head_step (CAS (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
+     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
 
 (** Atomic expressions *)
 Definition atomic (e: expr []) : bool :=
@@ -470,7 +463,7 @@ Qed.
 
 Lemma alloc_fresh e v σ :
   let l := fresh (dom _ σ) in
-  to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
+  to_val e = Some v → head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
 
 (** Equality and other typeclass stuff *)
@@ -497,7 +490,6 @@ Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool :=
      expr_beq e0 e0' && expr_beq e1 e1' && expr_beq e2 e2'
   | Fst e, Fst e' | Snd e, Snd e' | InjL e, InjL e' | InjR e, InjR e' |
     Fork e, Fork e' | Alloc e, Alloc e' | Load e, Load e' => expr_beq e e'
-  | Loc l, Loc l' => bool_decide (l = l')
   | _, _ => false
   end.
 Lemma expr_beq_correct {X} (e1 e2 : expr X) : expr_beq e1 e2 ↔ e1 = e2.
@@ -525,7 +517,7 @@ Program Instance heap_ectxi_lang :
   EctxiLanguage
     (heap_lang.expr []) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
   of_val := heap_lang.of_val; to_val := heap_lang.to_val;
-  fill_item := heap_lang.fill_item; 
+  fill_item := heap_lang.fill_item;
   atomic := heap_lang.atomic; head_step := heap_lang.head_step;
 |}.
 Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
diff --git a/heap_lang/lib/barrier/client.v b/heap_lang/lib/barrier/client.v
index 3276500cd..45366e9e0 100644
--- a/heap_lang/lib/barrier/client.v
+++ b/heap_lang/lib/barrier/client.v
@@ -27,7 +27,7 @@ Section client.
 
   Lemma worker_safe q (n : Z) (b y : loc) :
     (heap_ctx heapN ★ recv heapN N b (y_inv q y))
-    ⊢ WP worker n (%b) (%y) {{ _, True }}.
+    ⊢ WP worker n #b #y {{ _, True }}.
   Proof.
     iIntros "[#Hh Hrecv]". wp_lam. wp_let.
     wp_apply wait_spec; iFrame "Hrecv".
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 84a0c6978..c4ffb6504 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -95,7 +95,7 @@ Qed.
 (** Actual proofs *)
 Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
   heapN ⊥ N →
-  (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (%l))
+  (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ #l)
   ⊢ WP newbarrier #() {{ Φ }}.
 Proof.
   iIntros {HN} "[#? HΦ]".
@@ -121,7 +121,7 @@ Proof.
 Qed.
 
 Lemma signal_spec l P (Φ : val → iProp) :
-  (send l P ★ P ★ Φ #()) ⊢ WP signal (%l) {{ Φ }}.
+  (send l P ★ P ★ Φ #()) ⊢ WP signal #l {{ Φ }}.
 Proof.
   rewrite /signal /send /barrier_ctx.
   iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let.
@@ -136,7 +136,7 @@ Proof.
 Qed.
 
 Lemma wait_spec l P (Φ : val → iProp) :
-  (recv l P ★ (P -★ Φ #())) ⊢ WP wait (%l) {{ Φ }}.
+  (recv l P ★ (P -★ Φ #())) ⊢ WP wait #l {{ Φ }}.
 Proof.
   rename P into R; rewrite /recv /barrier_ctx.
   iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index f3973ad1b..3a517ebae 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -14,9 +14,9 @@ Lemma barrier_spec (heapN N : namespace) :
   heapN ⊥ N →
   ∃ recv send : loc → iProp -n> iProp,
     (∀ P, heap_ctx heapN ⊢ {{ True }} newbarrier #() {{ v,
-                             ∃ l : loc, v = LocV l ★ recv l P ★ send l P }}) ∧
-    (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ _, True }}) ∧
-    (∀ l P, {{ recv l P }} wait (LocV l) {{ _, P }}) ∧
+                             ∃ l : loc, v = #l ★ recv l P ★ send l P }}) ∧
+    (∀ l P, {{ send l P ★ P }} signal #l {{ _, True }}) ∧
+    (∀ l P, {{ recv l P }} wait #l {{ _, P }}) ∧
     (∀ l P Q, recv l (P ★ Q) ={N}=> recv l P ★ recv l Q) ∧
     (∀ l P Q, (P -★ Q) ⊢ (recv l P -★ recv l Q)).
 Proof.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 9de604041..09bec1ec5 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -49,7 +49,7 @@ Qed.
 
 Lemma newlock_spec N (R : iProp) Φ :
   heapN ⊥ N →
-  (heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ (LocV l)))
+  (heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ #l))
   ⊢ WP newlock #() {{ Φ }}.
 Proof.
   iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
@@ -61,7 +61,7 @@ Proof.
 Qed.
 
 Lemma acquire_spec l R (Φ : val → iProp) :
-  (is_lock l R ★ (locked l R -★ R -★ Φ #())) ⊢ WP acquire (%l) {{ Φ }}.
+  (is_lock l R ★ (locked l R -★ R -★ Φ #())) ⊢ WP acquire #l {{ Φ }}.
 Proof.
   iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
   iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
@@ -75,7 +75,7 @@ Proof.
 Qed.
 
 Lemma release_spec R l (Φ : val → iProp) :
-  (locked l R ★ R ★ Φ #()) ⊢ WP release (%l) {{ Φ }}.
+  (locked l R ★ R ★ Φ #()) ⊢ WP release #l {{ Φ }}.
 Proof.
   iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(%&#?&#?&Hγ)".
   rewrite /release. wp_let.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 5172ea364..454c1489c 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -53,7 +53,7 @@ Proof. solve_proper. Qed.
 Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
   to_val e = Some f →
   heapN ⊥ N →
-  (heap_ctx heapN ★ WP f #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ (%l))
+  (heap_ctx heapN ★ WP f #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ #l)
   ⊢ WP spawn e {{ Φ }}.
 Proof.
   iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
@@ -71,7 +71,7 @@ Proof.
 Qed.
 
 Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
-  (join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v) ⊢ WP join (%l) {{ Φ }}.
+  (join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v) ⊢ WP join #l {{ Φ }}.
 Proof.
   rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
   iLöb as "IH". wp_rec. wp_focus (! _)%E.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 3aeaf32f8..157125e22 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -25,13 +25,13 @@ Proof. exact: weakestpre.wp_bind. Qed.
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 Lemma wp_alloc_pst E σ e v Φ :
   to_val e = Some v →
-  (▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l)))
+  (▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LitV (LitLoc l))))
   ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
   iIntros {?}  "[HP HΦ]".
   (* TODO: This works around ssreflect bug #22. *)
   set (φ (e' : expr []) σ' ef := ∃ l,
-    ef = None ∧ e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
+    ef = None ∧ e' = Lit (LitLoc l) ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
   iApply (wp_lift_atomic_head_step (Alloc e) φ σ); try (by simpl; eauto);
     [by intros; subst φ; inv_head_step; eauto 8|].
   iFrame "HP". iNext. iIntros {v2 σ2 ef} "[% HP]".
@@ -42,7 +42,7 @@ Qed.
 
 Lemma wp_load_pst E σ l v Φ :
   σ !! l = Some v →
-  (▷ ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊢ WP Load (Loc l) @ E {{ Φ }}.
+  (▷ ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
     last (by intros; inv_head_step; eauto using to_of_val); simpl; by eauto.
@@ -51,7 +51,7 @@ Qed.
 Lemma wp_store_pst E σ l e v v' Φ :
   to_val e = Some v → σ !! l = Some v' →
   (▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Φ (LitV LitUnit)))
-  ⊢ WP Store (Loc l) e @ E {{ Φ }}.
+  ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
   intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
     ?right_id //; last (by intros; inv_head_step; eauto); simpl; by eauto.
@@ -60,7 +60,7 @@ Qed.
 Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
   (▷ ownP σ ★ ▷ (ownP σ -★ Φ (LitV $ LitBool false)))
-  ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
+  ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
     ?right_id //; last (by intros; inv_head_step; eauto);
@@ -70,7 +70,7 @@ Qed.
 Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
   (▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Φ (LitV $ LitBool true)))
-  ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
+  ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
     (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto);
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 1789ac8f3..1cb2cc05e 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -19,20 +19,20 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
+Coercion LitLoc : loc >-> base_lit.
+
 Coercion App : expr >-> Funclass.
 Coercion of_val : val >-> expr.
 
 Coercion BNamed : string >-> binder.
 Notation "<>" := BAnon : binder_scope.
 
-(* No scope for the values, does not conflict and scope is often not inferred properly. *)
+(* No scope for the values, does not conflict and scope is often not inferred
+properly. *)
 Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
-Notation "% l" := (LocV l) (at level 8, format "% l").
-Notation "# l" := (LitV l%Z%V) (at level 8, format "# l") : val_scope.
-Notation "% l" := (LocV l) (at level 8, format "% l") : val_scope.
 Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
-Notation "% l" := (Loc l) (at level 8, format "% l") : expr_scope.
 
+Check of_val'.
 Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
 Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope.
 
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index ff8c242c7..05d5668bc 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -21,7 +21,8 @@ Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
   Δ ⊢ heap_ctx N → nclose N ⊆ E →
   StripLaterEnvs Δ Δ' →
   (∀ l, ∃ Δ'',
-    envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧ Δ'' ⊢ Φ (LocV l)) →
+    envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
+    Δ'' ⊢ Φ (LitV (LitLoc l))) →
   Δ ⊢ WP Alloc e @ E {{ Φ }}.
 Proof.
   intros ???? HΔ; eapply wp_alloc; eauto.
@@ -35,7 +36,7 @@ Lemma tac_wp_load Δ Δ' N E i l q v Φ :
   StripLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   Δ' ⊢ Φ v →
-  Δ ⊢ WP Load (Loc l) @ E {{ Φ }}.
+  Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
   intros. eapply wp_load; eauto.
   rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
@@ -48,7 +49,7 @@ Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ :
   StripLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  Δ'' ⊢ Φ (LitV LitUnit) → Δ ⊢ WP Store (Loc l) e @ E {{ Φ }}.
+  Δ'' ⊢ Φ (LitV LitUnit) → Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
   intros. eapply wp_store; eauto.
   rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -61,7 +62,7 @@ Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
   StripLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
   Δ' ⊢ Φ (LitV (LitBool false)) →
-  Δ ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
+  Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. eapply wp_cas_fail; eauto.
   rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
@@ -74,7 +75,7 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l e1 v1 e2 v2 Φ :
   StripLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v1)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  Δ'' ⊢ Φ (LitV (LitBool true)) → Δ ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
+  Δ'' ⊢ Φ (LitV (LitBool true)) → Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
   intros. eapply wp_cas_suc; eauto.
   rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -115,7 +116,7 @@ Tactic Notation "wp_load" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
-    | Load (Loc ?l) =>
+    | Load (Lit (LitLoc ?l)) =>
        wp_bind K; eapply tac_wp_load;
          [iAssumption || fail 2 "wp_load: cannot find heap_ctx"
          |done || eauto with ndisj
@@ -145,7 +146,7 @@ Tactic Notation "wp_cas_fail" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
-    | CAS (Loc ?l) ?e1 ?e2 =>
+    | CAS (Lit (LitLoc ?l)) ?e1 ?e2 =>
        wp_bind K; eapply tac_wp_cas_fail;
          [wp_done || fail 2 "wp_cas_fail:" e1 "not a value"
          |wp_done || fail 2 "wp_cas_fail:" e2 "not a value"
@@ -162,7 +163,7 @@ Tactic Notation "wp_cas_suc" :=
   match goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
-    | CAS (Loc ?l) ?e1 ?e2 =>
+    | CAS (Lit (LitLoc ?l)) ?e1 ?e2 =>
        wp_bind K; eapply tac_wp_cas_suc;
          [wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
          |wp_done || fail 2 "wp_cas_suc:" e1 "not a value"
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index c3745ea7a..7dfaee028 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -41,8 +41,6 @@ Notation W := (WExpr H).
 (* Ground terms *)
 Global Instance do_wexpr_lit l : W (Lit l) (Lit l).
 Proof. done. Qed.
-Global Instance do_wexpr_loc l : W (Loc l) (Loc l).
-Proof. done. Qed.
 Global Instance do_wexpr_app e1 e2 e1r e2r :
   W e1 e1r → W e2 e2r → W (App e1 e2) (App e1r e2r).
 Proof. intros; red; f_equal/=; apply: do_wexpr. Qed.
@@ -159,8 +157,6 @@ Notation Sub := (WSubst x es H).
 (* Ground terms *)
 Global Instance do_wsubst_lit l : Sub (Lit l) (Lit l).
 Proof. done. Qed.
-Global Instance do_wsubst_loc l : Sub (Loc l) (Loc l).
-Proof. done. Qed.
 Global Instance do_wsubst_app e1 e2 e1r e2r :
   Sub e1 e1r → Sub e2 e2r → Sub (App e1 e2) (App e1r e2r).
 Proof. intros; red; f_equal/=; apply: do_wsubst. Qed.
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index 04b4817cf..796832ee3 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -32,7 +32,6 @@ Ltac reshape_val e tac :=
     let v1 := reshape_val e1 in let v2 := reshape_val e2 in constr:(PairV v1 v2)
   | InjL ?e => let v := reshape_val e in constr:(InjLV v)
   | InjR ?e => let v := reshape_val e in constr:(InjRV v)
-  | Loc ?l => constr:(LocV l)
   end in let v := go e in first [tac v | fail 2].
 
 Ltac reshape_expr e tac :=
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index da065422c..a96ddeaf7 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -20,7 +20,7 @@ Definition barrier_res γ (Φ : X → iProp) : iProp :=
 
 Lemma worker_spec e γ l (Φ Ψ : X → iProp) :
   (recv heapN N l (barrier_res γ Φ) ★ ∀ x, {{ Φ x }} e {{ _, Ψ x }})
-  ⊢ WP wait (%l) ;; e {{ _, barrier_res γ Ψ }}.
+  ⊢ WP wait #l ;; e {{ _, barrier_res γ Ψ }}.
 Proof.
   iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl".
   iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]".
-- 
GitLab