From 621aa83c54244f41796a80d93eff63be930487d7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 11 Feb 2024 18:04:51 +0100
Subject: [PATCH] Some clean up.

---
 _CoqProject                |  1 -
 theories/channel/channel.v |  2 +-
 theories/channel/proto.v   | 16 ++++++++--------
 theories/utils/skip.v      | 11 -----------
 4 files changed, 9 insertions(+), 21 deletions(-)
 delete mode 100644 theories/utils/skip.v

diff --git a/_CoqProject b/_CoqProject
index e46494d..843f066 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,7 +8,6 @@
 # Fixing this one requires Coq 8.19
 -arg -w -arg -argument-scope-delimiter
 
-theories/utils/skip.v
 theories/utils/llist.v
 theories/utils/compare.v
 theories/utils/contribution.v
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index e8d038e..2c53a5e 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -25,7 +25,7 @@ From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Export proofmode.
 From iris.heap_lang.lib Require Import spin_lock.
 From actris.channel Require Export proto.
-From actris.utils Require Import llist skip.
+From actris.utils Require Import llist.
 Set Default Proof Using "Type".
 
 Local Existing Instance spin_lock.
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 92c4c00..9e9dfcf 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -54,10 +54,17 @@ From actris.channel Require Import proto_model.
 Set Default Proof Using "Type".
 Export action.
 
+(** * Types *)
+Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
+Declare Scope proto_scope.
+Delimit Scope proto_scope with proto.
+Bind Scope proto_scope with iProto.
+Open Scope proto.
+
 (** * Setup of Iris's cameras *)
 Class protoG Σ V :=
   protoG_authG ::
-    inG Σ (excl_authR (laterO (proto (leibnizO V) (iPropO Σ) (iPropO Σ)))).
+    inG Σ (excl_authR (laterO (iProto Σ V))).
 
 Definition protoΣ V := #[
   GFunctor (authRF (optionURF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF)))))
@@ -65,13 +72,6 @@ Definition protoΣ V := #[
 Global Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
 Proof. solve_inG. Qed.
 
-(** * Types *)
-Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
-Declare Scope proto_scope.
-Delimit Scope proto_scope with proto.
-Bind Scope proto_scope with iProto.
-Open Scope proto.
-
 (** * Messages *)
 Section iMsg.
   Set Primitive Projections.
diff --git a/theories/utils/skip.v b/theories/utils/skip.v
deleted file mode 100644
index 76c38b3..0000000
--- a/theories/utils/skip.v
+++ /dev/null
@@ -1,11 +0,0 @@
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
-
-Definition skipN : val :=
-  rec: "go" "n" := if: #0 < "n" then "go" ("n" - #1) else #().
-
-Lemma skipN_spec `{heapGS Σ} Φ (n : nat) : ▷^n (Φ #()) -∗ WP skipN #n {{ Φ }}.
-Proof.
-  iIntros "HΦ". iInduction n as [|n] "IH"; wp_rec; wp_pures; [done|].
-  rewrite Z.sub_1_r Nat2Z.inj_succ Z.pred_succ. by iApply "IH".
-Qed.
-- 
GitLab