Commit a07c0c2a authored by Robbert Krebbers's avatar Robbert Krebbers

Rename.

parent cf1f0776
Pipeline #27498 passed with stage
in 19 minutes and 14 seconds
......@@ -23,7 +23,7 @@ theories/logrel/environments.v
theories/logrel/term_types.v
theories/logrel/session_types.v
theories/logrel/operators.v
theories/logrel/typing_judgment.v
theories/logrel/term_typing_judgment.v
theories/logrel/subtyping_rules.v
theories/logrel/term_typing_rules.v
theories/logrel/examples/double.v
......
From iris.algebra Require Import frac.
From iris.heap_lang.lib Require Export par spin_lock.
From actris.channel Require Import proofmode.
From actris.logrel Require Export typing_judgment session_types.
From actris.logrel Require Export term_typing_judgment session_types.
From actris.logrel Require Import environments.
Definition prog : val := λ: "c",
......
......@@ -3,7 +3,7 @@ From iris.bi.lib Require Import core.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import metatheory.
From iris.heap_lang.lib Require Export spawn par assert.
From actris.logrel Require Export subtyping typing_judgment session_types.
From actris.logrel Require Export subtyping term_typing_judgment session_types.
From actris.logrel Require Import environments.
From actris.utils Require Import switch.
From actris.channel Require Import proofmode.
......
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