From fef73ef67320be2b3da945a3e2d372026dee52f3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 26 May 2020 14:57:47 +0200
Subject: [PATCH] Fix.

---
 theories/channel/channel.v   | 2 +-
 theories/logrel/term_types.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 736ab7a..e02f321 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -21,7 +21,7 @@ In this file we define the three message-passing connectives:
 
 It is additionaly shown that the channel ownership [c ↣ prot] is closed under
 the subprotocol relation [⊑] *)
-From iris.heap_lang Require Export lifting notation.
+From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib Require Import spin_lock.
 From actris.channel Require Export proto.
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index 5ac9800..b2ab312 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -34,7 +34,7 @@ non-expansiveness of these type formers is proved. This is important in order to
 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 iris.heap_lang Require Export lib.spin_lock.
 From actris.logrel Require Export model.
 From actris.channel Require Export channel.
 
-- 
GitLab