diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 736ab7a6efc42251363725a5cc693e55c4e14362..e02f3214ea65a4f4611809c41839c59898cf53d4 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 5ac980072f93bef4730e485f3b71920d21c9c88d..b2ab312f4ce6f6bb71a0c21c676ae6fb2a7ef5ff 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.