diff --git a/_CoqProject b/_CoqProject
index b21005506fcd2bb5f5044b44ef88a9548246641e..c505f549bafc79e09cd42c84a6303ba69c987c00 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -140,6 +140,7 @@ iris/proofmode/frame_instances.v
 iris/proofmode/monpred.v
 iris/proofmode/modalities.v
 iris/proofmode/modality_instances.v
+iris/proofmode/proofmode.v
 
 iris_heap_lang/locations.v
 iris_heap_lang/lang.v
diff --git a/iris/proofmode/proofmode.v b/iris/proofmode/proofmode.v
new file mode 100644
index 0000000000000000000000000000000000000000..6b5d01b87c38ccb68dc8ed48cc178985337839c5
--- /dev/null
+++ b/iris/proofmode/proofmode.v
@@ -0,0 +1,11 @@
+(** The main proofmode file taht everyone should import.
+Unless you are working with the guts of the proofmode, do not import any other
+file from this folder! *)
+From iris.proofmode Require Export ltac_tactics.
+(* This [Require Import] is not a no-op: it exports typeclass instances from
+these files. *)
+From iris.proofmode Require Import class_instances class_instances_later
+  class_instances_updates class_instances_embedding
+  class_instances_plainly class_instances_internal_eq.
+From iris.proofmode Require Import frame_instances modality_instances.
+From iris.prelude Require Import options.
diff --git a/iris/proofmode/tactics.v b/iris/proofmode/tactics.v
index f7680f074e4b30ff099cf9ab1235c10dcd2d3c51..4aa7545a017ab7b857c83e6805a5d0339d69f6d4 100644
--- a/iris/proofmode/tactics.v
+++ b/iris/proofmode/tactics.v
@@ -1,8 +1,4 @@
-From iris.proofmode Require Export ltac_tactics.
-(* This [Require Import] is not a no-op: it exports typeclass instances from
-these files. *)
-From iris.proofmode Require Import class_instances class_instances_later
-  class_instances_updates class_instances_embedding
-  class_instances_plainly class_instances_internal_eq.
-From iris.proofmode Require Import frame_instances modality_instances.
+(* This file is *deprecated*. It exists just to give people some time to adjust their code.
+Directly import [iris.proofmode.proofmode] instead. *)
+From iris.proofmode Require Export proofmode.
 From iris.prelude Require Import options.