From a34eb5819224c4d44f8f5a1488dd3cb29087ff29 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 16 Dec 2016 12:35:55 +0100
Subject: [PATCH] remove unused file type_incl

---
 _CoqProject                 |  1 -
 theories/typing/function.v  |  2 +-
 theories/typing/product.v   |  2 +-
 theories/typing/sum.v       |  3 +--
 theories/typing/type_incl.v | 44 -------------------------------------
 5 files changed, 3 insertions(+), 49 deletions(-)
 delete mode 100644 theories/typing/type_incl.v

diff --git a/_CoqProject b/_CoqProject
index d1abaecb..2935afb5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -24,7 +24,6 @@ theories/lang/races.v
 theories/lang/tactics.v
 theories/lang/wp_tactics.v
 theories/typing/type.v
-theories/typing/type_incl.v
 theories/typing/perm.v
 theories/typing/typing.v
 theories/typing/lft_contexts.v
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 73ffb52b..986660f7 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import hoare.
 From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import type_incl typing lft_contexts type_context cont_context.
+From lrust.typing Require Import typing lft_contexts type_context cont_context.
 
 Section fn.
   Context `{typeG Σ}.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index e01a07fb..df8e3942 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import perm type_incl.
+From lrust.typing Require Import perm.
 
 Section product.
   Context `{typeG Σ}.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 138f15ee..6b39fd7f 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,8 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import fractional.
 From lrust.lifetime Require Import borrow frac_borrow.
-From lrust.typing Require Export type.
-From lrust.typing Require Import type_incl.
+From lrust.typing Require Export type perm.
 
 Section sum.
   Context `{typeG Σ}.
diff --git a/theories/typing/type_incl.v b/theories/typing/type_incl.v
deleted file mode 100644
index 4cd87f37..00000000
--- a/theories/typing/type_incl.v
+++ /dev/null
@@ -1,44 +0,0 @@
-From iris.base_logic Require Import big_op.
-From iris.program_logic Require Import hoare.
-From lrust.typing Require Export type perm.
-From lrust.lifetime Require Import frac_borrow borrow.
-
-Section ty_incl.
-  Context `{typeG Σ}.
-
-  Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
-    ∀ tid, lft_ctx -∗ ρ tid ={⊤}=∗
-      (□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ∗
-      (□ ∀ κ E l, ty1.(ty_shr) κ tid E l →
-       (* [ty_incl] needs to prove something about the length of the
-          object when it is shared. We place this property under the
-          hypothesis that [ty2.(ty_shr)] holds, so that the [!] type
-          is still included in any other. *)
-                  ty2.(ty_shr) κ tid E l ∗ ⌜ty1.(ty_size) = ty2.(ty_size)⌝).
-
-  Lemma ty_incl_trans ρ θ ty1 ty2 ty3 :
-    ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ∗ θ) ty1 ty3.
-  Proof.
-    iIntros (H12 H23 tid) "#LFT [H1 H2]".
-    iMod (H12 with "LFT H1") as "[#H12 #H12']".
-    iMod (H23 with "LFT H2") as "[#H23 #H23']".
-    iModIntro; iSplit; iIntros "!#*H1".
-    - by iApply "H23"; iApply "H12".
-    - iDestruct ("H12'" $! _ _ _ with "H1") as "[H2 %]".
-      iDestruct ("H23'" $! _ _ _ with "H2") as "[$ %]".
-      iPureIntro. congruence.
-  Qed.
-
-  Lemma ty_incl_weaken ρ θ ty1 ty2 :
-    ρ ⇒ θ → ty_incl θ ty1 ty2 → ty_incl ρ ty1 ty2.
-  Proof.
-    iIntros (Hρθ Hρ' tid) "#LFT H". iApply (Hρ' with "LFT>"). iApply (Hρθ with "LFT H").
-  Qed.
-
-  Lemma ty_incl_perm_incl ρ ty1 ty2 ν :
-    ty_incl ρ ty1 ty2 → ρ ∗ ν ◁ ty1 ⇒ ν ◁ ty2.
-  Proof.
-    iIntros (Hincl tid) "#LFT [Hρ Hty1]". iMod (Hincl with "LFT Hρ") as "[#Hownincl _]".
-    unfold has_type. destruct (eval_expr ν); last done. by iApply "Hownincl".
-  Qed.
-End ty_incl.
\ No newline at end of file
-- 
GitLab