use iris.proofmode.proofmode as the new root module for the proofmode

_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

iris/proofmode/proofmode.v

+(** 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.

iris/proofmode/tactics.v

-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.