From 9af5ee4fa2eeb2f54809b2f0f36f1940695a9083 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 20 Dec 2016 19:16:07 +0100
Subject: [PATCH] cleanup

---
 opam.pins              |  2 +-
 theories/typing/type.v | 30 ------------------------------
 2 files changed, 1 insertion(+), 31 deletions(-)

diff --git a/opam.pins b/opam.pins
index 90d82d5a..9d848526 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq e2b843075894275afd52c19c83e4f5f812afdbab
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq adfa07525e071b2a47aed37dac276aa38c10099d
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 1160c6a6..d62a06cf 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -98,36 +98,6 @@ Section type.
     rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
   Qed.
 
-  Lemma na_own_acc F2 F1 tid :
-    F2 ⊆ F1 →
-    na_own tid F1 -∗ na_own tid F2 ∗
-           (na_own tid F2 -∗ na_own tid F1).
-  Proof.
-    intros HF. assert (F1 = F2 ∪ (F1 ∖ F2)) as -> by exact: union_difference_L.
-    rewrite na_own_union; last by set_solver+.
-    iIntros "[$ $]". auto.
-  Qed.
-
-(*  Lemma shr_locsE_get_tok l n F tid :
-    shr_locsE l n ⊆ F →
-    na_own tid F -∗ na_own tid (shr_locsE l n) ∗ 
-         (na_own tid (shr_locsE l n) -∗ na_own tid F).
-  Proof.
-    intros HF.
-    assert (F = shr_locsE l n ∪ (F ∖ shr_locsE l n)) as -> by exact: union_difference_L.
-    rewrite na_own_union; last by set_solver+.
-    iIntros "[$ $]". by iIntros "?".
-  Qed.
-
-  Lemma shr_locsE_get_tokS l n F tid :
-    shr_locsE l (n + 1) ⊆ F →
-    na_own tid F -∗ na_own tid (shr_locsE l n) ∗ 
-         (na_own tid (shr_locsE l n) -∗ na_own tid F).
-  Proof.
-    intros HF. apply shr_locsE_get_tok. rewrite <-HF.
-    apply shr_locsE_subseteq. omega.
-  Qed.
-*)
   (** Copy types *)
   Class Copy (t : type) := {
     copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
-- 
GitLab