From 528c3ed5777fd5b6f3d0086c061ba026f2b342b7 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Tue, 11 Jun 2019 19:33:28 +0200
Subject: [PATCH] Refactoring: Renamed stype->proto files

---
 _CoqProject                                 | 6 +++---
 theories/examples/examples.v                | 2 +-
 theories/examples/list_sort.v               | 2 +-
 theories/examples/proofs.v                  | 2 +-
 theories/examples/proofs_enc.v              | 2 +-
 theories/proto/branching.v                  | 2 +-
 theories/proto/{stype_def.v => proto_def.v} | 0
 theories/proto/{stype_enc.v => proto_enc.v} | 2 +-
 theories/proto/{stype.v => proto_specs.v}   | 2 +-
 9 files changed, 10 insertions(+), 10 deletions(-)
 rename theories/proto/{stype_def.v => proto_def.v} (100%)
 rename theories/proto/{stype_enc.v => proto_enc.v} (98%)
 rename theories/proto/{stype.v => proto_specs.v} (99%)

diff --git a/_CoqProject b/_CoqProject
index 5e5ad4f..04256a8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,9 +6,9 @@ theories/proto/list.v
 theories/proto/channel.v
 theories/proto/involutive.v
 theories/proto/side.v
-theories/proto/stype_def.v
-theories/proto/stype.v
-theories/proto/stype_enc.v
+theories/proto/proto_def.v
+theories/proto/proto_specs.v
+theories/proto/proto_enc.v
 theories/proto/branching.v
 theories/examples/examples.v
 theories/examples/proofs.v
diff --git a/theories/examples/examples.v b/theories/examples/examples.v
index 4b6976d..bf59602 100644
--- a/theories/examples/examples.v
+++ b/theories/examples/examples.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.base_logic Require Import invariants.
-From osiris.proto Require Import stype.
+From osiris.proto Require Import proto_specs.
 
 Section Examples.
   Context `{!heapG Σ} (N : namespace).
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index 9f49286..630702e 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -4,8 +4,8 @@ Require Import Omega.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.proto Require Import list channel stype_enc.
 From iris.base_logic Require Import invariants.
+From osiris.proto Require Import list channel proto_enc.
 
 Section ListSortExample.
   Context `{!heapG Σ} `{logrelG val Σ} (N : namespace).
diff --git a/theories/examples/proofs.v b/theories/examples/proofs.v
index dc679f7..0e472cf 100644
--- a/theories/examples/proofs.v
+++ b/theories/examples/proofs.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.base_logic Require Import invariants.
-From osiris.proto Require Import stype.
+From osiris.proto Require Import proto_specs.
 From osiris.examples Require Import examples.
 
 Section ExampleProofs.
diff --git a/theories/examples/proofs_enc.v b/theories/examples/proofs_enc.v
index 186c706..608ecfb 100644
--- a/theories/examples/proofs_enc.v
+++ b/theories/examples/proofs_enc.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
-From osiris.proto Require Import stype_enc.
+From osiris.proto Require Import proto_enc.
 From osiris.examples Require Import examples.
 
 Section ExampleProofsEnc.
diff --git a/theories/proto/branching.v b/theories/proto/branching.v
index 7c552dc..b511fa2 100644
--- a/theories/proto/branching.v
+++ b/theories/proto/branching.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
-From osiris.proto Require Export stype_enc.
+From osiris.proto Require Export proto_enc.
 
 Section DualBranch.
   Context `{PROP : bi}.
diff --git a/theories/proto/stype_def.v b/theories/proto/proto_def.v
similarity index 100%
rename from theories/proto/stype_def.v
rename to theories/proto/proto_def.v
diff --git a/theories/proto/stype_enc.v b/theories/proto/proto_enc.v
similarity index 98%
rename from theories/proto/stype_enc.v
rename to theories/proto/proto_enc.v
index de6637f..05a775e 100644
--- a/theories/proto/stype_enc.v
+++ b/theories/proto/proto_enc.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
-From osiris.proto Require Export encodable stype.
+From osiris.proto Require Export encodable proto_specs.
 
 Section DualStypeEnc.
   Context `{EncDec V} `{PROP: bi} .
diff --git a/theories/proto/stype.v b/theories/proto/proto_specs.v
similarity index 99%
rename from theories/proto/stype.v
rename to theories/proto/proto_specs.v
index 48df209..c6d1277 100644
--- a/theories/proto/stype.v
+++ b/theories/proto/proto_specs.v
@@ -6,7 +6,7 @@ From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
 From osiris.base_logic Require Import auth_excl.
-From osiris.proto Require Export stype_def.
+From osiris.proto Require Export proto_def.
 From osiris.proto Require Export channel.
 
 Class logrelG A Σ := {
-- 
GitLab