Commit a15377fd authored by Robbert Krebbers's avatar Robbert Krebbers

Rename telescope file.

parent 49ac37b8
...@@ -19,7 +19,7 @@ theories/examples/map.v ...@@ -19,7 +19,7 @@ theories/examples/map.v
theories/examples/map_reduce.v theories/examples/map_reduce.v
theories/examples/subprotocols.v theories/examples/subprotocols.v
theories/logrel/model.v theories/logrel/model.v
theories/logrel/kind_tele.v theories/logrel/telescopes.v
theories/logrel/subtyping.v theories/logrel/subtyping.v
theories/logrel/environments.v theories/logrel/environments.v
theories/logrel/term_types.v theories/logrel/term_types.v
......
...@@ -3,7 +3,7 @@ protocols. It includes session types for sending and receiving with session ...@@ -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 polymorphism, as well as n-ary choice. Recursive protocols are defined in
the model.v file. *) the model.v file. *)
From iris.algebra Require Export gmap. 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. From actris.channel Require Export channel.
Definition lmsg Σ := iMsg Σ. Definition lmsg Σ := iMsg Σ.
......
...@@ -35,7 +35,7 @@ use these type formers to define recursive types. *) ...@@ -35,7 +35,7 @@ use these type formers to define recursive types. *)
From iris.bi.lib Require Import core. From iris.bi.lib Require Import core.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Export spin_lock. 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. From actris.channel Require Export channel.
Definition lty_unit {Σ} : ltty Σ := Ltty (λ w, w = #() %I). Definition lty_unit {Σ} : ltty Σ := Ltty (λ w, w = #() %I).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment