From a15377fd79e14afc70b78ac429e8960ef677b98d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 May 2020 14:12:58 +0200
Subject: [PATCH] Rename telescope file.

---
 _CoqProject                                   | 2 +-
 theories/logrel/session_types.v               | 2 +-
 theories/logrel/{kind_tele.v => telescopes.v} | 0
 theories/logrel/term_types.v                  | 2 +-
 4 files changed, 3 insertions(+), 3 deletions(-)
 rename theories/logrel/{kind_tele.v => telescopes.v} (100%)

diff --git a/_CoqProject b/_CoqProject
index cbdb539..6b5dd96 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -19,7 +19,7 @@ theories/examples/map.v
 theories/examples/map_reduce.v
 theories/examples/subprotocols.v
 theories/logrel/model.v
-theories/logrel/kind_tele.v
+theories/logrel/telescopes.v
 theories/logrel/subtyping.v
 theories/logrel/environments.v
 theories/logrel/term_types.v
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index e772044..d7d5f50 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -3,7 +3,7 @@ protocols. It includes session types for sending and receiving with session
 polymorphism, as well as n-ary choice. Recursive protocols are defined in
 the model.v file. *)
 From iris.algebra Require Export gmap.
-From actris.logrel Require Export model kind_tele.
+From actris.logrel Require Export model telescopes.
 From actris.channel Require Export channel.
 
 Definition lmsg Σ := iMsg Σ.
diff --git a/theories/logrel/kind_tele.v b/theories/logrel/telescopes.v
similarity index 100%
rename from theories/logrel/kind_tele.v
rename to theories/logrel/telescopes.v
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index b29cec1..aa3ad2a 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -35,7 +35,7 @@ use these type formers to define recursive types. *)
 From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Export spin_lock.
-From actris.logrel Require Export model kind_tele.
+From actris.logrel Require Export model.
 From actris.channel Require Export channel.
 
 Definition lty_unit {Σ} : ltty Σ := Ltty (λ w, ⌜ w = #() ⌝%I).
-- 
GitLab