diff --git a/_CoqProject b/_CoqProject
index e64289f5538f7ab358f022e554fdb2391fd24fe7..1c6bf74ca80877a9eeb8858e30a552b7395cc1c1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -47,6 +47,7 @@ theories/bi/lib/core.v
 theories/base_logic/upred.v
 theories/base_logic/bi.v
 theories/base_logic/derived.v
+theories/base_logic/proofmode.v
 theories/base_logic/base_logic.v
 theories/base_logic/double_negation.v
 theories/base_logic/lib/iprop.v
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index b485d1343abfbf5bc81456ed979f51b2dae67cce..5059f6575fa7f53f83a3c406545d7ea703a88aca 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,6 +1,5 @@
-From iris.base_logic Require Export derived.
+From iris.base_logic Require Export derived proofmode.
 From iris.bi Require Export bi.
-From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 
 (* The trick of having multiple [uPred] modules, which are all exported in
@@ -11,42 +10,3 @@ Module Import uPred.
   Export derived.uPred.
   Export bi.bi.
 End uPred.
-
-(* Setup of the proof mode *)
-Section class_instances.
-Context {M : ucmraT}.
-Implicit Types P Q R : uPred M.
-
-Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
-  @IntoPure (uPredI M) (✓ a) (✓ a).
-Proof. by rewrite /IntoPure discrete_valid. Qed.
-
-Global Instance from_pure_cmra_valid {A : cmraT} af (a : A) :
-  @FromPure (uPredI M) af (✓ a) (✓ a).
-Proof.
-  rewrite /FromPure. eapply bi.pure_elim; [by apply affinely_if_elim|]=> ?.
-  rewrite -cmra_valid_intro //.
-Qed.
-
-Global Instance from_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 →
-  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
-Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
-  IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
-  FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros ? H. rewrite /FromAnd (is_op a) ownM_op.
-  destruct H; by rewrite persistent_and_sep.
-Qed.
-
-Global Instance into_and_ownM p (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros. apply intuitionistically_if_mono. by rewrite (is_op a) ownM_op sep_and.
-Qed.
-
-Global Instance into_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
-End class_instances.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
new file mode 100644
index 0000000000000000000000000000000000000000..6caa4627b3f435395fb0917bf1295258aff8c3db
--- /dev/null
+++ b/theories/base_logic/proofmode.v
@@ -0,0 +1,43 @@
+From iris.base_logic Require Export derived.
+From iris.algebra Require Import proofmode_classes.
+
+Import base_logic.bi.uPred.
+
+(* Setup of the proof mode *)
+Section class_instances.
+Context {M : ucmraT}.
+Implicit Types P Q R : uPred M.
+
+Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
+  @IntoPure (uPredI M) (✓ a) (✓ a).
+Proof. by rewrite /IntoPure discrete_valid. Qed.
+
+Global Instance from_pure_cmra_valid {A : cmraT} af (a : A) :
+  @FromPure (uPredI M) af (✓ a) (✓ a).
+Proof.
+  rewrite /FromPure. eapply bi.pure_elim; [by apply bi.affinely_if_elim|]=> ?.
+  rewrite -uPred.cmra_valid_intro //.
+Qed.
+
+Global Instance from_sep_ownM (a b1 b2 : M) :
+  IsOp a b1 b2 →
+  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
+Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
+  IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
+  FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  intros ? H. rewrite /FromAnd (is_op a) ownM_op.
+  destruct H; by rewrite bi.persistent_and_sep.
+Qed.
+
+Global Instance into_and_ownM p (a b1 b2 : M) :
+  IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+  intros. apply bi.intuitionistically_if_mono. by rewrite (is_op a) ownM_op bi.sep_and.
+Qed.
+
+Global Instance into_sep_ownM (a b1 b2 : M) :
+  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
+End class_instances.