Fix.

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.

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.