diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 54c7ace7273e9714fc353693d19c93185bd780d1..6636e38e5106667137a1834a5df1f058f3b35c22 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -2,7 +2,6 @@
 (** A resource algebra for the specification programs. *)
 From iris.algebra Require Import auth excl gmap agree list frac.
 From iris.bi Require Export fractional.
-From iris.base_logic Require Import gen_heap.
 From iris.base_logic Require Export invariants.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang primitive_laws.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 2d79d34446bba0d49c76bf3305e536c88b3b2ee4..cf519ed264647ab6d4ee0daee6dec10cd7ee4aa3 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -1,7 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Rules for updating the specification program. *)
 From iris.algebra Require Import auth excl frac agree gmap list.
-From iris.base_logic.lib Require Import gen_heap.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Export lang notation tactics.
 From reloc.logic Require Export spec_ra.