From 136c0066e7866f7170c1034a859b8dc922d0a64f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 26 Jul 2021 19:57:21 +0200
Subject: [PATCH] use iris.proofmode.proofmode as the new root module for the
 proofmode

---
 _CoqProject                |  1 +
 iris/proofmode/proofmode.v | 11 +++++++++++
 iris/proofmode/tactics.v   | 10 +++-------
 3 files changed, 15 insertions(+), 7 deletions(-)
 create mode 100644 iris/proofmode/proofmode.v

diff --git a/_CoqProject b/_CoqProject
index b21005506..c505f549b 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 000000000..6b5d01b87
--- /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 f7680f074..4aa7545a0 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.
-- 
GitLab