From 989f0ffd7b8dffdea9e19a72f2f7a1e473020b72 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 27 Oct 2020 16:26:30 +0100
Subject: [PATCH] =?UTF-8?q?remove=20'l=20=E2=86=A6=20-'=20notation?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It is barely used and causes a lot of confusion when used like 'l ↦ - * P'
---
 theories/base_logic/lib/gen_heap.v | 15 ---------------
 1 file changed, 15 deletions(-)

diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 6d6caee52..42d01936c 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -126,10 +126,6 @@ Local Notation "l ↦{ q } v" := (mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
 Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
 
-Local Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
-  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
-Local Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
-
 Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
   ⊢ |==> ∃ _ : gen_heapG L V Σ, gen_heap_interp σ.
 Proof.
@@ -175,17 +171,6 @@ Section gen_heap.
     iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
   Qed.
 
-  Global Instance ex_mapsto_fractional l : Fractional (λ q, l ↦{q} -)%I.
-  Proof.
-    intros p q. iSplit.
-    - iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
-    - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
-      iDestruct (mapsto_agree with "H1 H2") as %->. iExists v2. by iFrame.
-  Qed.
-  Global Instance ex_mapsto_as_fractional l q :
-    AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I q.
-  Proof. split. done. apply _. Qed.
-
   Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
   Proof.
     rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
-- 
GitLab