From 0975c0ac44d2ef6226f0fb088a69b52875f837dc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 15 Apr 2019 15:18:19 +0200
Subject: [PATCH] Remove deadcode `symbol_ctx`.

---
 theories/logrel_heaplang/lib/symbol_adt.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/theories/logrel_heaplang/lib/symbol_adt.v b/theories/logrel_heaplang/lib/symbol_adt.v
index 1acc807..fbbe575 100644
--- a/theories/logrel_heaplang/lib/symbol_adt.v
+++ b/theories/logrel_heaplang/lib/symbol_adt.v
@@ -65,9 +65,6 @@ Section ltyped_symbol_adt.
   Definition symbol_inv (γ : gname) (l : loc) : iProp Σ :=
     (∃ n : nat, l ↦ #n ∗ counter γ n)%I.
 
-  Definition symbol_ctx (γ : gname) (l : loc) : iProp Σ :=
-    inv symbol_adtN (symbol_inv γ l).
-
   Definition lty_symbol (γ : gname) : lty Σ := Lty (λ w,
     ∃ n : nat, ⌜w = #n⌝ ∧ symbol γ n)%I.
 
-- 
GitLab