From 538d0804263a14a6ff27467989f4e773234e68ff Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 7 Jul 2019 16:24:59 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20osiris=20=E2=86=92=20actris.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 _CoqProject                          | 2 +-
 experimental/producer_consumer.v     | 4 ++--
 theories/channel/channel.v           | 2 +-
 theories/channel/proofmode.v         | 2 +-
 theories/channel/proto_channel.v     | 6 +++---
 theories/examples/loop_sort.v        | 6 +++---
 theories/examples/map.v              | 4 ++--
 theories/examples/map_reduce.v       | 6 +++---
 theories/examples/sort.v             | 4 ++--
 theories/examples/sort_client.v      | 6 +++---
 theories/examples/sort_elem.v        | 4 ++--
 theories/examples/sort_elem_client.v | 6 +++---
 12 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index d44c0b0..89039c0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,4 @@
--Q theories osiris
+-Q theories actris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 theories/utils/auth_excl.v
 theories/utils/list.v
diff --git a/experimental/producer_consumer.v b/experimental/producer_consumer.v
index ed3d4d8..c011e32 100644
--- a/experimental/producer_consumer.v
+++ b/experimental/producer_consumer.v
@@ -1,8 +1,8 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Import assert.
-From osiris.utils Require Import list compare spin_lock.
+From actris.utils Require Import list compare spin_lock.
 
 Definition qenqueue : val := λ: "q" "v", #().
 Definition qdequeue : val := λ: "q", #().
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index c2e7096..28ed362 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -1,7 +1,7 @@
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import excl auth list.
-From osiris.utils Require Import auth_excl list.
+From actris.utils Require Import auth_excl list.
 Set Default Proof Using "Type".
 
 Inductive side := Left | Right.
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 8645c4a..cb4d487 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Export proofmode notation.
 From iris.proofmode Require Export tactics.
-From osiris Require Export proto_channel.
+From actris Require Export proto_channel.
 From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 
 (* TODO: strip laters *)
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index 0326743..c14a455 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -1,9 +1,9 @@
-From osiris.channel Require Export channel.
-From osiris.channel Require Import proto_model.
+From actris.channel Require Export channel.
+From actris.channel Require Import proto_model.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import auth excl.
-From osiris.utils Require Import auth_excl.
+From actris.utils Require Import auth_excl.
 Export action.
 
 Definition start_chan : val := λ: "f",
diff --git a/theories/examples/loop_sort.v b/theories/examples/loop_sort.v
index a779c92..04aa8cc 100644
--- a/theories/examples/loop_sort.v
+++ b/theories/examples/loop_sort.v
@@ -1,8 +1,8 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel.
+From actris.channel Require Import proto_channel.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.utils Require Import list.
-From osiris.examples Require Import sort.
+From actris.utils Require Import list.
+From actris.examples Require Import sort.
 
 Definition loop_sort_service : val :=
   rec: "go" "c" :=
diff --git a/theories/examples/map.v b/theories/examples/map.v
index f134e62..1282c31 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -1,6 +1,6 @@
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation lib.spin_lock.
-From osiris.utils Require Import list contribution.
+From actris.utils Require Import list contribution.
 From iris.algebra Require Import gmultiset.
 
 Definition map_worker : val :=
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 4a015a2..56176cc 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -1,8 +1,8 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.utils Require Import list compare contribution.
-From osiris.examples Require Import map sort_elem sort_elem_client.
+From actris.utils Require Import list compare contribution.
+From actris.examples Require Import map sort_elem sort_elem_client.
 From iris.algebra Require Import gmultiset.
 From Coq Require Import SetoidPermutation.
 
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index 5ab7100..6d29875 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -1,7 +1,7 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.utils Require Import list compare.
+From actris.utils Require Import list compare.
 
 Definition lmerge : val :=
   rec: "go" "cmp" "ys" "zs" :=
diff --git a/theories/examples/sort_client.v b/theories/examples/sort_client.v
index ec3de22..1353293 100644
--- a/theories/examples/sort_client.v
+++ b/theories/examples/sort_client.v
@@ -1,8 +1,8 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.utils Require Import list compare.
-From osiris.examples Require Import sort.
+From actris.utils Require Import list compare.
+From actris.examples Require Import sort.
 
 Definition sort_client : val := λ: "cmp" "xs",
   let: "c" := start_chan sort_service in
diff --git a/theories/examples/sort_elem.v b/theories/examples/sort_elem.v
index def7cb9..171a707 100644
--- a/theories/examples/sort_elem.v
+++ b/theories/examples/sort_elem.v
@@ -1,8 +1,8 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Import assert.
-From osiris.utils Require Import list compare.
+From actris.utils Require Import list compare.
 
 Definition cont := true.
 Definition stop := false.
diff --git a/theories/examples/sort_elem_client.v b/theories/examples/sort_elem_client.v
index 1c12e47..7662c6c 100644
--- a/theories/examples/sort_elem_client.v
+++ b/theories/examples/sort_elem_client.v
@@ -1,9 +1,9 @@
 From stdpp Require Import sorting.
-From osiris.channel Require Import proto_channel proofmode.
+From actris.channel Require Import proto_channel proofmode.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Import assert.
-From osiris.utils Require Import list compare.
-From osiris.examples Require Import sort_elem.
+From actris.utils Require Import list compare.
+From actris.examples Require Import sort_elem.
 
 Definition send_all : val :=
   rec: "go" "c" "xs" :=
-- 
GitLab