From f23e484b689b34197d7954c3b6a9b9aa120d7919 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Thu, 4 Apr 2019 14:16:03 +0200
Subject: [PATCH] Minor clean-up

---
 theories/auth_excl.v | 27 +++------------------------
 theories/typing.v    | 11 ++---------
 2 files changed, 5 insertions(+), 33 deletions(-)

diff --git a/theories/auth_excl.v b/theories/auth_excl.v
index 02d21b5..37431c2 100644
--- a/theories/auth_excl.v
+++ b/theories/auth_excl.v
@@ -4,28 +4,6 @@ From iris.algebra Require Import excl auth.
 From iris.base_logic.lib Require Import auth.
 Set Default Proof Using "Type".
 
-(* Definition exclUR (A : Type) : ucmraT := *)
-(*   optionUR (exclR (leibnizC A)). *)
-
-(* Definition to_auth_excl {A : Type} (a : A) : exclUR A := *)
-(*   Excl' (a: leibnizC A). *)
-
-(* Section auth_excl. *)
-
-(* Class auth_exclG (A : Type) (Σ :gFunctors) := *)
-(*   AuthExclG { *)
-(*       exclG_authG :> authG Σ (exclUR A); *)
-(*     }. *)
-
-(* Definition auth_exclΣ (A : Type) : gFunctors := *)
-(*   #[GFunctor (authR (exclUR A))]. *)
-
-(* Instance subG_auth_exclG {Σ} (A : Type) : *)
-(*   subG (auth_exclΣ) Σ → (auth_exclG) Σ. *)
-(* Proof. solve_inG. Qed. *)
-
-(* End auth_excl. *)
-
 Definition exclUR (A : Type) : ucmraT :=
   optionUR (exclR (leibnizC A)).
 
@@ -46,7 +24,7 @@ Definition to_auth_excl {A : Type} (a : A) : exclUR A :=
 
 
 Section auth_excl.
-  Context `{!auth_exclG A Σ} (N : namespace).
+  Context `{!auth_exclG A Σ}.
 
   Lemma excl_eq γ x y :
     own γ (● to_auth_excl y) -∗ own γ (◯  to_auth_excl x) -∗ ⌜x = y⌝%I.
@@ -63,7 +41,8 @@ Section auth_excl.
   Qed.
   
   Lemma excl_update γ x y z :
-    own γ (● to_auth_excl y) -∗ own γ (◯  to_auth_excl x) -∗ |==> own γ (● to_auth_excl z) ∗ own γ (◯  to_auth_excl z).
+    own γ (● to_auth_excl y) -∗ own γ (◯  to_auth_excl x) ==∗
+    own γ (● to_auth_excl z) ∗ own γ (◯  to_auth_excl z).
   Proof.
     iIntros "Hauth Hfrag".
     iDestruct (own_update_2 with "Hauth Hfrag") as "H".
diff --git a/theories/typing.v b/theories/typing.v
index d632e61..fad620e 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -1,22 +1,15 @@
-From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From stdpp Require Import gmap.
-From iris.base_logic Require Import invariants.
-Require Import FunctionalExtensionality.
 
 Section typing.
 
-  (* Sides *)
   Inductive side : Set :=
   | Left
   | Right.
 
-  (* Session Types *)
   Inductive stype :=
   | TEnd
-  | TSend (P : heap_lang.val → Prop) (sτ : heap_lang.val → stype)
-  | TRecv (P : heap_lang.val → Prop) (sτ : heap_lang.val → stype).
+  | TSend (P : val → Prop) (sτ : val → stype)
+  | TRecv (P : val → Prop) (sτ : val → stype).
 
   Fixpoint dual_stype (sτ :stype) :=
     match sτ with
-- 
GitLab