diff --git a/_CoqProject b/_CoqProject
index 598e82936d254ab21ad1d2030f603a210e92a06e..ecff6175ecf2720c282fc830b9b6dcac2c62f5a7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,6 +15,7 @@
 -arg -w -arg -redundant-canonical-projection
 
 iris/prelude/options.v
+iris/prelude/prelude.v
 iris/algebra/monoid.v
 iris/algebra/cmra.v
 iris/algebra/big_op.v
@@ -25,7 +26,6 @@ iris/algebra/view.v
 iris/algebra/auth.v
 iris/algebra/gmap.v
 iris/algebra/ofe.v
-iris/algebra/base.v
 iris/algebra/dra.v
 iris/algebra/cofe_solver.v
 iris/algebra/agree.v
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 135865d7e4fcadd73bb07440b7cd34494aa68930..87f734ef5a6b1820371618a57e3ccb3337892d79 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export base.
+From iris.prelude Require Export prelude.
 From iris.prelude Require Import options.
 Set Primitive Projections.
 
diff --git a/iris/algebra/base.v b/iris/prelude/prelude.v
similarity index 100%
rename from iris/algebra/base.v
rename to iris/prelude/prelude.v
diff --git a/iris/program_logic/ectx_language.v b/iris/program_logic/ectx_language.v
index a76f590edcf6cff23fa1f8fba2289b525ca8f81f..df53a018598d2e472de426455c596f3dcaa5ea33 100644
--- a/iris/program_logic/ectx_language.v
+++ b/iris/program_logic/ectx_language.v
@@ -1,6 +1,6 @@
 (** An axiomatization of evaluation-context based languages, including a proof
     that this gives rise to a "language" in the Iris sense. *)
-From iris.algebra Require Export base.
+From iris.prelude Require Export prelude.
 From iris.program_logic Require Import language.
 From iris.prelude Require Import options.
 
diff --git a/iris/program_logic/ectxi_language.v b/iris/program_logic/ectxi_language.v
index e3a245b2e4912303db0bed39c08ef405452a9878..bbb6d90523c5ec1675a33fb6fc8bd80dd3349430 100644
--- a/iris/program_logic/ectxi_language.v
+++ b/iris/program_logic/ectxi_language.v
@@ -1,6 +1,6 @@
 (** An axiomatization of languages based on evaluation context items, including
     a proof that these are instances of general ectx-based languages. *)
-From iris.algebra Require Export base.
+From iris.prelude Require Export prelude.
 From iris.program_logic Require Import language ectx_language.
 From iris.prelude Require Import options.
 
diff --git a/iris/proofmode/base.v b/iris/proofmode/base.v
index 5a969fea020a852e90c570fc14d6705255698481..0c9168eeb9e5eb64eb48090fbff99790f28a1da5 100644
--- a/iris/proofmode/base.v
+++ b/iris/proofmode/base.v
@@ -1,6 +1,6 @@
 From Coq Require Export Ascii.
 From stdpp Require Export strings.
-From iris.algebra Require Export base.
+From iris.prelude Require Export prelude.
 From iris.prelude Require Import options.
 
 (** * Utility definitions used by the proofmode *)
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index e185690dc538dc25a5d149fe0731876c52d169d2..fb132f827b81ef04a9500fd0f6ce4a976f401690 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export base.
+From iris.prelude Require Export prelude.
 From iris.bi Require Export bi.
 From iris.proofmode Require Import base.
 From iris.prelude Require Import options.
diff --git a/iris_heap_lang/locations.v b/iris_heap_lang/locations.v
index 7cca50788928e1b14fead5d0599d624751d8e762..6da303478011e4cfcdbe272d793f5953b46ac644 100644
--- a/iris_heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -1,5 +1,5 @@
 From stdpp Require Import countable numbers gmap.
-From iris.algebra Require Import base.
+From iris.prelude Require Export prelude.
 From iris.prelude Require Import options.
 
 Record loc := { loc_car : Z }.