diff --git a/_CoqProject b/_CoqProject
index deeba11357170af130f63048f33ade0aa48ea2de..8f1e85df39ef852e04ad5bf10d05a7ed739c9db6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -24,6 +24,7 @@ theories/algebra/local_updates.v
 theories/algebra/gset.v
 theories/algebra/coPset.v
 theories/algebra/deprecated.v
+theories/algebra/proofmode_classes.v
 theories/bi/interface.v
 theories/bi/derived.v
 theories/bi/big_op.v
@@ -39,7 +40,6 @@ theories/base_logic/soundness.v
 theories/base_logic/double_negation.v
 theories/base_logic/deprecated.v
 theories/base_logic/proofmode.v
-theories/base_logic/proofmode_classes.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v
 theories/base_logic/lib/saved_prop.v
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 07cff4db7210b803ad3f2d6c5d734a1a7f024ec7..607d0cae2e47e8d33d283067e5b186eaac473dd4 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export excl local_updates.
-From iris.base_logic Require Import base_logic proofmode_classes.
+From iris.algebra Require Import proofmode_classes.
+From iris.base_logic Require Import base_logic.
 Set Default Proof Using "Type".
 
 Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 253ceae52723335105931354163ebf75be1a871e..d76652cc9f5877b92821a4f23c94fde1b079b667 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
-From iris.base_logic Require Import proofmode_classes.
+From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 
 Notation frac := Qp (only parsing).
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 1d564f3ac4933bdbddc5ab1e1b9c7260a4c25b56..92de4e2355c78c466bc23c5332f9304a841a0ccb 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export frac auth.
 From iris.algebra Require Export updates local_updates.
-From iris.base_logic Require Import proofmode_classes.
+From iris.algebra Require Import proofmode_classes.
 
 Definition frac_authR (A : cmraT) : cmraT :=
   authR (optionUR (prodR fracR A)).
diff --git a/theories/base_logic/proofmode_classes.v b/theories/algebra/proofmode_classes.v
similarity index 96%
rename from theories/base_logic/proofmode_classes.v
rename to theories/algebra/proofmode_classes.v
index e24217f6c216e043678fe41c428fa5c511fc5545..1c033303b74fb5f677051a335cbd36e0742ead94 100644
--- a/theories/base_logic/proofmode_classes.v
+++ b/theories/algebra/proofmode_classes.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Export classes.
-From iris.base_logic Require Export base_logic.
+From iris.algebra Require Export cmra.
 
 (* There are various versions of [IsOp] with different modes:
 
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 308331a0466e19fe6bd6a0b42f21526eb4afd6d3..b4d22032689d24d634f8ab3b77bca0f5f7e43512 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import iprod gmap.
 From iris.base_logic.lib Require Export iprop.
-From iris.base_logic Require Import proofmode_classes.
+From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index ac7c11bef72ddaa2271754f5438f9923f1a43f40..40f79a6a760b468bc7c03b9c612711001397988a 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Export base_logic.
 From iris.proofmode Require Export tactics.
-From iris.base_logic Require Import proofmode_classes.
+From iris.algebra Require Import proofmode_classes.
 Import uPred.
 Import bi.