From 708450ba72b6e95e6ca1224f76745b8325bcf1c1 Mon Sep 17 00:00:00 2001 From: jihgfee <jihgfee@gmail.com> Date: Mon, 14 Oct 2019 18:19:41 -0400 Subject: [PATCH] Bumped move of Atomic to Iris --- _CoqProject | 1 - theories/channel/channel.v | 3 ++- theories/utils/misc.v | 10 ---------- 3 files changed, 2 insertions(+), 12 deletions(-) delete mode 100644 theories/utils/misc.v diff --git a/_CoqProject b/_CoqProject index 5aa77d4..1dbcef5 100644 --- a/_CoqProject +++ b/_CoqProject @@ -5,7 +5,6 @@ theories/utils/llist.v theories/utils/compare.v theories/utils/contribution.v theories/utils/group.v -theories/utils/misc.v theories/channel/channel.v theories/channel/proto_model.v theories/channel/proto_channel.v diff --git a/theories/channel/channel.v b/theories/channel/channel.v index f7bf1dc..6ae5317 100644 --- a/theories/channel/channel.v +++ b/theories/channel/channel.v @@ -17,8 +17,9 @@ and [chan_own]: [s] ([Left] or [Right]) has contents [vs]. *) From iris.heap_lang Require Import proofmode notation. From iris.heap_lang.lib Require Import spin_lock. +From iris.heap_lang Require Import lifting. From iris.algebra Require Import excl auth list. -From actris.utils Require Import auth_excl llist misc. +From actris.utils Require Import auth_excl llist. Set Default Proof Using "Type". Inductive side := Left | Right. diff --git a/theories/utils/misc.v b/theories/utils/misc.v deleted file mode 100644 index 86a9f3c..0000000 --- a/theories/utils/misc.v +++ /dev/null @@ -1,10 +0,0 @@ -From iris.heap_lang Require Import notation. -Set Default Proof Using "Type". - -(** MOVE TO IRIS *) -Global Instance fst_atomic a v1 v2 : Atomic a (Fst (v1,v2)%V). -Proof. - apply strongly_atomic_atomic, ectx_language_atomic; - [inversion 1; naive_solver - |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver]. -Qed. -- GitLab