From 43a1a90f65771cf0ee901dff6b82e3757f5be340 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 11 Sep 2019 20:39:03 +0200
Subject: [PATCH] Reorder Requires so that we do not depend of Export bugs.

The general idea is to first import/export modules which are further
than the current one, and then import/export modules which are close
dependencies.

This commit tries to use the same order of imports for every file, and
describes the convention in ProofGuide.md. There is one exception,
where we do not follow said convention: in program_logic/weakestpre.v,
using that order would break printing of texan triples (??).
---
 ProofGuide.md                                  | 18 ++++++++++++++++++
 tests/atomic.v                                 |  4 ++--
 tests/heap_lang2.v                             |  2 +-
 tests/ipm_paper.v                              |  2 +-
 tests/list_reverse.v                           |  2 +-
 tests/mosel_paper.v                            |  2 +-
 tests/one_shot.v                               |  4 ++--
 tests/one_shot_once.v                          |  4 ++--
 tests/tree_sum.v                               |  2 +-
 theories/algebra/auth.v                        |  2 +-
 theories/algebra/big_op.v                      |  2 +-
 theories/algebra/cmra.v                        |  2 +-
 theories/algebra/cmra_big_op.v                 |  4 ++--
 theories/algebra/coPset.v                      |  2 +-
 theories/algebra/csum.v                        |  2 +-
 theories/algebra/frac_auth.v                   |  3 +--
 theories/algebra/functions.v                   |  2 +-
 theories/algebra/gmap.v                        |  5 ++---
 theories/algebra/gmultiset.v                   |  2 +-
 theories/algebra/gset.v                        |  2 +-
 theories/algebra/list.v                        |  4 ++--
 theories/algebra/namespace_map.v               |  5 ++---
 theories/algebra/proofmode_classes.v           |  4 ++--
 theories/algebra/ufrac_auth.v                  |  6 ++----
 theories/base_logic/base_logic.v               |  2 +-
 theories/base_logic/bi.v                       |  2 +-
 theories/base_logic/bupd_alt.v                 |  2 +-
 theories/base_logic/derived.v                  |  4 ++--
 theories/base_logic/lib/auth.v                 |  4 ++--
 theories/base_logic/lib/boxes.v                | 10 +++++-----
 .../base_logic/lib/cancelable_invariants.v     |  4 ++--
 theories/base_logic/lib/fancy_updates.v        |  6 +++---
 .../base_logic/lib/fancy_updates_from_vs.v     |  4 ++--
 theories/base_logic/lib/gen_heap.v             |  4 ++--
 theories/base_logic/lib/invariants.v           |  6 +++---
 theories/base_logic/lib/iprop.v                |  2 +-
 theories/base_logic/lib/na_invariants.v        |  4 ++--
 theories/base_logic/lib/own.v                  |  3 +--
 theories/base_logic/lib/proph_map.v            |  2 +-
 theories/base_logic/lib/saved_prop.v           |  4 ++--
 theories/base_logic/lib/sts.v                  |  4 ++--
 theories/base_logic/lib/viewshifts.v           |  2 +-
 theories/base_logic/lib/wsat.v                 | 16 ++++++++--------
 theories/base_logic/proofmode.v                |  2 +-
 theories/base_logic/upred.v                    |  5 ++---
 theories/bi/big_op.v                           |  4 ++--
 theories/bi/embedding.v                        |  2 +-
 theories/bi/interface.v                        |  2 +-
 theories/bi/lib/atomic.v                       |  2 +-
 theories/bi/weakestpre.v                       |  2 +-
 theories/heap_lang/adequacy.v                  |  6 +++---
 theories/heap_lang/array.v                     |  4 ++--
 theories/heap_lang/lang.v                      |  6 +++---
 theories/heap_lang/lib/arith.v                 |  2 +-
 theories/heap_lang/lib/assert.v                |  2 +-
 theories/heap_lang/lib/atomic_heap.v           |  8 ++++----
 theories/heap_lang/lib/counter.v               |  6 +++---
 theories/heap_lang/lib/diverge.v               |  2 +-
 theories/heap_lang/lib/increment.v             |  4 ++--
 theories/heap_lang/lib/lock.v                  |  3 +--
 theories/heap_lang/lib/par.v                   |  2 +-
 theories/heap_lang/lib/spawn.v                 |  6 +++---
 theories/heap_lang/lib/spin_lock.v             |  4 ++--
 theories/heap_lang/lib/ticket_lock.v           |  4 ++--
 theories/heap_lang/lifting.v                   |  4 ++--
 theories/heap_lang/locations.v                 |  2 +-
 theories/heap_lang/metatheory.v                |  2 +-
 theories/heap_lang/proofmode.v                 |  4 ++--
 theories/heap_lang/total_adequacy.v            |  2 +-
 theories/program_logic/adequacy.v              |  4 ++--
 theories/program_logic/atomic.v                |  6 +++---
 theories/program_logic/ectx_lifting.v          |  2 +-
 theories/program_logic/hoare.v                 |  4 ++--
 theories/program_logic/lifting.v               |  2 +-
 theories/program_logic/ownp.v                  |  4 ++--
 theories/program_logic/total_adequacy.v        |  4 ++--
 theories/program_logic/total_ectx_lifting.v    |  3 +--
 theories/program_logic/total_lifting.v         |  2 +-
 theories/program_logic/total_weakestpre.v      |  4 ++--
 theories/program_logic/weakestpre.v            |  4 +++-
 theories/proofmode/base.v                      |  2 +-
 theories/proofmode/classes.v                   |  2 +-
 theories/proofmode/environments.v              |  4 ++--
 theories/proofmode/ltac_tactics.v              |  7 +++----
 theories/proofmode/modalities.v                |  2 +-
 theories/proofmode/notation.v                  |  2 +-
 86 files changed, 166 insertions(+), 156 deletions(-)

diff --git a/ProofGuide.md b/ProofGuide.md
index af06f6ab3..81fb49820 100644
--- a/ProofGuide.md
+++ b/ProofGuide.md
@@ -6,6 +6,24 @@ This complements the tactic documentation for the [proof mode](ProofMode.md) and
 [HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in
 the [style guide](StyleGuide.md).
 
+## Order of `Requires`
+
+In Coq, declarations in modules imported later may override the
+previous definition. Therefore, in order to make sure the most
+relevant declarations and notations always take priority, we recommend
+importing dependencies from the furthest to the closest.
+
+In particular, when importing Iris, Stdpp and Coq stdlib modules, we
+recommend importing in the following order:
+- Coq
+- stdpp
+- iris.bi
+- iris.proofmode
+- iris.algebra
+- iris.base_logic
+- iris.program_logic
+- iris.heap_lang
+
 ## Combinators for functors
 
 In Iris, the type of propositions [iProp] is described by the solution to the
diff --git a/tests/atomic.v b/tests/atomic.v
index 236ec1e71..6e3b57077 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,6 +1,6 @@
-From iris.heap_lang Require Export lifting notation.
-From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export atomic.
+From iris.heap_lang Require Export lifting notation.
 From iris.heap_lang Require Import proofmode notation atomic_heap.
 Set Default Proof Using "Type".
 
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index f2e7050b0..85dcae1bc 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -1,7 +1,7 @@
 (* Test yet another way of importing heap_lang modules that used to break
 printing *)
-From iris.heap_lang Require Export lifting notation.
 From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Export lifting notation.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 79ec0d82a..d279aded7 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -3,8 +3,8 @@
 Interactive Proofs in Higher-Order Concurrent Separation Logic
 Robbert Krebbers, Amin Timany and Lars Birkedal
 POPL 2017 *)
-From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import base_logic.
 From iris.program_logic Require Export hoare.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 95850a2d4..ba12c8599 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -1,7 +1,7 @@
 (** Correctness of in-place list reversal *)
+From iris.proofmode Require Export tactics.
 From iris.program_logic Require Export total_weakestpre weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/tests/mosel_paper.v b/tests/mosel_paper.v
index 25211740a..bb9eb5b42 100644
--- a/tests/mosel_paper.v
+++ b/tests/mosel_paper.v
@@ -5,8 +5,8 @@ Separation Logic
 Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti,
 Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
 ICFP 2018 *)
-From iris.proofmode Require Import tactics monpred.
 From iris.bi Require Import monpred.
+From iris.proofmode Require Import tactics monpred.
 
 Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
   P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, (P ∗ Φ a) ∨ (P ∗ Ψ a).
diff --git a/tests/one_shot.v b/tests/one_shot.v
index dd9f08ed0..03441f827 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -1,8 +1,8 @@
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl agree csum.
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
-From iris.algebra Require Import excl agree csum.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Import par.
 Set Default Proof Using "Type".
 
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 5aec75458..ee19d8581 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -1,8 +1,8 @@
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import frac agree csum.
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
-From iris.algebra Require Import frac agree csum.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Import par.
 Set Default Proof Using "Type".
 
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index c959fbf03..d7f1865a9 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -1,6 +1,6 @@
+From iris.proofmode Require Export tactics.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index b2dad6a87..ecd650d58 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -1,7 +1,7 @@
+From iris.proofmode Require Import tactics.
 From iris.algebra Require Export frac agree local_updates.
 From iris.algebra Require Import proofmode_classes.
 From iris.base_logic Require Import base_logic.
-From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 (** Authoritative CMRA with fractional authoritative parts. [auth] has 3 types
diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index cb9109bfc..fb4badc23 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Export monoid.
 From stdpp Require Export functions gmap gmultiset.
+From iris.algebra Require Export monoid.
 Set Default Proof Using "Type*".
 Local Existing Instances monoid_ne monoid_assoc monoid_comm
   monoid_left_id monoid_right_id monoid_proper
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 635bb9267..8fbfcdddf 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Export ofe monoid.
 From stdpp Require Import finite.
+From iris.algebra Require Export ofe monoid.
 Set Default Proof Using "Type".
 
 Class PCore (A : Type) := pcore : A → option A.
diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v
index 6bbf5244d..65467b604 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Export big_op cmra.
 From stdpp Require Import gmap gmultiset.
+From iris.algebra Require Export big_op cmra.
 Set Default Proof Using "Type*".
 
 (** Option *)
@@ -33,4 +33,4 @@ Proof.
   { rewrite big_opMS_empty. set_solver. }
   rewrite -equiv_None big_opMS_disj_union big_opMS_singleton equiv_None op_None IH.
   set_solver.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index 326c0251d..0cae57b57 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -1,6 +1,6 @@
+From stdpp Require Export sets coPset.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-From stdpp Require Export sets coPset.
 Set Default Proof Using "Type".
 (** This is pretty much the same as algebra/gset, but I was not able to
 generalize the construction without breaking canonical structures. *)
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 2749d4ec8..86d121530 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export cmra.
-From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import local_updates.
+From iris.base_logic Require Import base_logic.
 Set Default Proof Using "Type".
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 3f7d27c3c..46d1e180d 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -1,5 +1,4 @@
-From iris.algebra Require Export frac auth.
-From iris.algebra Require Export updates local_updates.
+From iris.algebra Require Export frac auth updates local_updates.
 From iris.algebra Require Import proofmode_classes.
 
 (** Authoritative CMRA where the NON-authoritative parts can be fractional.
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index 3e66c877b..80e65d794 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -1,6 +1,6 @@
+From stdpp Require Import finite.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates.
-From stdpp Require Import finite.
 Set Default Proof Using "Type".
 
 Definition discrete_fun_insert `{EqDecision A} {B : A → ofeT}
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 38fb0a48a..021184995 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -1,8 +1,7 @@
-From iris.algebra Require Export cmra.
 From stdpp Require Export list gmap.
-From iris.algebra Require Import updates local_updates.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import updates local_updates proofmode_classes.
 From iris.base_logic Require Import base_logic.
-From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 
 Section cofe.
diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index bd4637134..7572718e9 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -1,6 +1,6 @@
+From stdpp Require Export sets gmultiset countable.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-From stdpp Require Export sets gmultiset countable.
 Set Default Proof Using "Type".
 
 (* The multiset union CMRA *)
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index b0b7fc512..14773b60e 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -1,6 +1,6 @@
+From stdpp Require Export sets gmap mapset.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-From stdpp Require Export sets gmap mapset.
 Set Default Proof Using "Type".
 
 (* The union CMRA *)
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index d97f640aa..e89df5de0 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -1,7 +1,7 @@
-From iris.algebra Require Export cmra.
 From stdpp Require Export list.
-From iris.base_logic Require Import base_logic.
+From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
+From iris.base_logic Require Import base_logic.
 Set Default Proof Using "Type".
 
 Section cofe.
diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index 93c2ff117..72949d1b2 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -1,7 +1,6 @@
-From iris.algebra Require Export gmap coPset local_updates.
 From stdpp Require Import namespaces.
-From iris.algebra Require Import updates.
-From iris.algebra Require Import proofmode_classes.
+From iris.algebra Require Export gmap coPset local_updates.
+From iris.algebra Require Import updates proofmode_classes.
 Set Default Proof Using "Type".
 
 (** The camera [namespace_map A] over a camera [A] provides the connectives
diff --git a/theories/algebra/proofmode_classes.v b/theories/algebra/proofmode_classes.v
index 7ccebbe78..c87bc6fa2 100644
--- a/theories/algebra/proofmode_classes.v
+++ b/theories/algebra/proofmode_classes.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Export classes.
 From iris.algebra Require Export cmra.
+From iris.proofmode Require Export classes.
 
 (* There are various versions of [IsOp] with different modes:
 
@@ -51,4 +51,4 @@ Proof. by constructor. Qed.
 (* This one has a higher precendence than [is_op_op] so we get a [+] instead of
 an [â‹…]. *)
 Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
-Proof. done. Qed.
\ No newline at end of file
+Proof. done. Qed.
diff --git a/theories/algebra/ufrac_auth.v b/theories/algebra/ufrac_auth.v
index cec6d972f..af7a5c07f 100644
--- a/theories/algebra/ufrac_auth.v
+++ b/theories/algebra/ufrac_auth.v
@@ -16,11 +16,9 @@ difference:
 - We no longer have the [â—¯U{1} a] is the exclusive fragmental element (cf.
   [frac_auth_frag_validN_op_1_l]).
 *)
-From iris.algebra Require Export auth frac.
-From iris.algebra Require Import ufrac.
-From iris.algebra Require Export updates local_updates.
-From iris.algebra Require Import proofmode_classes.
 From Coq Require Import QArith Qcanon.
+From iris.algebra Require Export auth frac updates local_updates.
+From iris.algebra Require Import ufrac proofmode_classes.
 
 Definition ufrac_authR (A : cmraT) : cmraT :=
   authR (optionUR (prodR ufracR A)).
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 5059f6575..13c4da994 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,5 +1,5 @@
-From iris.base_logic Require Export derived proofmode.
 From iris.bi Require Export bi.
+From iris.base_logic Require Export derived proofmode.
 Set Default Proof Using "Type".
 
 (* The trick of having multiple [uPred] modules, which are all exported in
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 11a1a6a40..7c86fd444 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -43,7 +43,7 @@ Proof.
   - exact: @exist_intro.
   - exact: @exist_elim.
   - exact: sep_mono.
-  - exact: True_sep_1. 
+  - exact: True_sep_1.
   - exact: True_sep_2.
   - exact: sep_comm'.
   - exact: sep_assoc'.
diff --git a/theories/base_logic/bupd_alt.v b/theories/base_logic/bupd_alt.v
index 9cc3208a9..67d04dc7a 100644
--- a/theories/base_logic/bupd_alt.v
+++ b/theories/base_logic/bupd_alt.v
@@ -1,5 +1,5 @@
-From iris.base_logic Require Export base_logic.
 From iris.proofmode Require Import tactics.
+From iris.base_logic Require Export base_logic.
 
 (** This file contains an alternative version of basic updates, that is
 expression in terms of just the plain modality [â– ]. *)
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 0adcc1a5c..3c9527a6f 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,7 +1,7 @@
-From iris.base_logic Require Export bi.
 From iris.bi Require Export bi.
+From iris.base_logic Require Export bi.
 Set Default Proof Using "Type".
-Import bi base_logic.bi.uPred.
+Import bi.bi base_logic.bi.uPred.
 
 (** Derived laws for Iris-specific primitive connectives (own, valid).
     This file does NOT unseal! *)
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index c5a8b494a..0d754209f 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -1,7 +1,7 @@
-From iris.base_logic.lib Require Export invariants.
+From iris.proofmode Require Import tactics.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
-From iris.proofmode Require Import tactics.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 7de868396..1aa38e78b 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -1,6 +1,6 @@
-From iris.base_logic.lib Require Export invariants.
-From iris.algebra Require Import excl auth gmap agree.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl auth gmap agree.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
 
@@ -131,7 +131,7 @@ Proof.
   iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
   iInv N as (b) "[>Hγ _]".
-  iDestruct (big_opM_delete _ f _ false with "Hf")
+  iDestruct (big_sepM_delete _ f _ false with "Hf")
     as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
   iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
   iModIntro. iSplitL "Hγ"; first iExists false; eauto.
@@ -148,7 +148,7 @@ Lemma slice_fill E q f γ P Q :
 Proof.
   iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iInv N as (b') "[>Hγ _]".
-  iDestruct (big_opM_delete _ f _ false with "Hf")
+  iDestruct (big_sepM_delete _ f _ false with "Hf")
     as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
   iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
   iModIntro. iSplitL "Hγ HQ"; first (iNext; iExists true; by iFrame).
@@ -165,7 +165,7 @@ Lemma slice_empty E q f P Q γ :
 Proof.
   iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iInv N as (b) "[>Hγ HQ]".
-  iDestruct (big_opM_delete _ f with "Hf")
+  iDestruct (big_sepM_delete _ f with "Hf")
     as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
   iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
   iFrame "HQ".
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 78288c7e0..9fe581759 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -1,7 +1,7 @@
-From iris.base_logic.lib Require Export invariants.
 From iris.bi.lib Require Import fractional.
-From iris.algebra Require Export frac.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Export frac.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 6dfaa0d0c..024f6410a 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -1,8 +1,8 @@
-From iris.base_logic.lib Require Export own.
 From stdpp Require Export coPset.
-From iris.base_logic.lib Require Import wsat.
-From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.base_logic.lib Require Export own.
+From iris.base_logic.lib Require Import wsat.
 Set Default Proof Using "Type".
 Export invG.
 Import uPred.
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index b47fa0df6..a5c376e16 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -1,9 +1,9 @@
 (* This file shows that the fancy update can be encoded in terms of the
 view shift, and that the laws of the fancy update can be derived from the
 laws of the view shift. *)
-From iris.base_logic Require Export base_logic.
-From iris.proofmode Require Import tactics.
 From stdpp Require Export coPset.
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Export base_logic.
 Set Default Proof Using "Type*".
 
 Section fupd.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 18ba74aba..6a3c44d0b 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -1,8 +1,8 @@
-From iris.algebra Require Import auth gmap frac agree namespace_map.
 From stdpp Require Export namespaces.
-From iris.base_logic.lib Require Export own.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth gmap frac agree namespace_map.
+From iris.base_logic.lib Require Export own.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index cadd6f231..b00b42241 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -1,8 +1,8 @@
-From iris.base_logic.lib Require Export fancy_updates.
 From stdpp Require Export namespaces.
-From iris.base_logic.lib Require Import wsat.
-From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import gmap.
+From iris.base_logic.lib Require Export fancy_updates.
+From iris.base_logic.lib Require Import wsat.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 809bfe640..269b15c9b 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -1,6 +1,6 @@
-From iris.base_logic Require Export base_logic.
 From iris.algebra Require Import gmap.
 From iris.algebra Require cofe_solver.
+From iris.base_logic Require Export base_logic.
 Set Default Proof Using "Type".
 
 (** In this file we construct the type [iProp] of propositions of the Iris
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 680d34295..eff3c4abc 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -1,6 +1,6 @@
-From iris.base_logic.lib Require Export invariants.
-From iris.algebra Require Import gset coPset.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import gset coPset.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 822b32f30..ba33ca2f3 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -1,6 +1,5 @@
-From iris.algebra Require Import functions gmap.
+From iris.algebra Require Import functions gmap proofmode_classes.
 From iris.base_logic.lib Require Export iprop.
-From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index 28962d6cb..4891e0b9e 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -1,6 +1,6 @@
+From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth excl list gmap.
 From iris.base_logic.lib Require Export own.
-From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 2af2c2712..af76fb789 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -1,7 +1,7 @@
-From iris.base_logic Require Export own.
-From iris.algebra Require Import agree.
 From stdpp Require Import gmap.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import agree.
+From iris.base_logic Require Export own.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 6004e1b4b..ad55707f2 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -1,6 +1,6 @@
-From iris.base_logic.lib Require Export invariants.
-From iris.algebra Require Export sts.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Export sts.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index a727317d2..5fe481ad4 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -1,5 +1,5 @@
-From iris.base_logic.lib Require Export invariants.
 From iris.proofmode Require Import tactics.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 
 Definition vs `{!invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 6ffb41ff7..1c380e86d 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -1,7 +1,7 @@
-From iris.base_logic.lib Require Export own.
 From stdpp Require Export coPset.
-From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.base_logic.lib Require Export own.
 Set Default Proof Using "Type".
 
 (** All definitions in this file are internal to [fancy_updates] with the
@@ -129,9 +129,9 @@ Proof.
   rewrite /ownI /wsat -!lock.
   iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[Hw HI]".
   iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
-  iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
+  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
   - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
-    iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
+    iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
     iFrame "HI"; eauto.
   - iDestruct (ownE_singleton_twice with "[$HiE $HiE']") as %[].
 Qed.
@@ -140,9 +140,9 @@ Proof.
   rewrite /ownI /wsat -!lock.
   iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[Hw HI]".
   iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
-  iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
+  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
   - iDestruct (ownD_singleton_twice with "[$]") as %[].
-  - iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
+  - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
     iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
 Qed.
 
@@ -165,7 +165,7 @@ Proof.
   iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
   iExists (<[i:=P]>I); iSplitL "Hw".
   { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
-  iApply (big_opM_insert _ I); first done.
+  iApply (big_sepM_insert _ I); first done.
   iFrame "HI". iLeft. by rewrite /ownD; iFrame.
 Qed.
 
@@ -188,7 +188,7 @@ Proof.
   rewrite -/(ownD _). iFrame "HD".
   iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
   { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
-  iApply (big_opM_insert _ I); first done.
+  iApply (big_sepM_insert _ I); first done.
   iFrame "HI". by iRight.
 Qed.
 End wsat.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index 944b92e84..c5eba535b 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -1,5 +1,5 @@
-From iris.base_logic Require Export derived.
 From iris.algebra Require Import proofmode_classes.
+From iris.base_logic Require Export derived.
 
 Import base_logic.bi.uPred.
 
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index b861d2284..b2bf5f05c 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,7 +1,6 @@
-From iris.algebra Require Export cmra updates.
-From iris.bi Require Import notation.
 From stdpp Require Import finite.
-From Coq.Init Require Import Nat.
+From iris.bi Require Import notation.
+From iris.algebra Require Export cmra updates.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|] : core.
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption] : core.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 6120bf009..e938f99eb 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1,6 +1,6 @@
-From iris.algebra Require Export big_op.
-From iris.bi Require Import derived_laws_sbi.
 From stdpp Require Import countable fin_sets functions.
+From iris.bi Require Import derived_laws_sbi.
+From iris.algebra Require Export big_op.
 Set Default Proof Using "Type".
 Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 2410b808b..cd9fe751c 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Import monoid.
 From iris.bi Require Import interface derived_laws_sbi big_op plainly updates.
+From iris.algebra Require Import monoid.
 
 Class Embed (A B : Type) := embed : A → B.
 Arguments embed {_ _ _} _%I : simpl never.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 3d3ea3b86..4eb80f6c7 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Export ofe.
 From iris.bi Require Export notation.
+From iris.algebra Require Export ofe.
 Set Primitive Projections.
 
 Section bi_mixin.
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index bcfc613bc..a66e00c3b 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -1,6 +1,6 @@
+From stdpp Require Import coPset namespaces.
 From iris.bi Require Export bi updates laterable.
 From iris.bi.lib Require Import fixpoint.
-From stdpp Require Import coPset namespaces.
 From iris.proofmode Require Import coq_tactics tactics reduction.
 Set Default Proof Using "Type".
 
diff --git a/theories/bi/weakestpre.v b/theories/bi/weakestpre.v
index 387b24bf8..d6de4370c 100644
--- a/theories/bi/weakestpre.v
+++ b/theories/bi/weakestpre.v
@@ -1,6 +1,6 @@
 From stdpp Require Export coPset.
-From iris.program_logic Require Import language.
 From iris.bi Require Import interface derived_connectives.
+From iris.program_logic Require Import language.
 
 Inductive stuckness := NotStuck | MaybeStuck.
 
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index d3b20324a..da8ba0adc 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -1,8 +1,8 @@
-From iris.program_logic Require Export weakestpre adequacy.
+From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.
-From iris.heap_lang Require Import proofmode notation.
 From iris.base_logic.lib Require Import proph_map.
-From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre adequacy.
+From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
 Class heapPreG Σ := HeapPreG {
diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index 15331b9e8..31d63f27b 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -1,8 +1,8 @@
+From stdpp Require Import fin_maps.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lifting.
 From iris.heap_lang Require Import tactics notation.
-From iris.proofmode Require Import tactics.
-From stdpp Require Import fin_maps.
 Set Default Proof Using "Type".
 
 (** This file defines the [array] connective, a version of [mapsto] that works
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 4371dc237..4a99a3c32 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -1,8 +1,8 @@
-From iris.program_logic Require Export language ectx_language ectxi_language.
-From iris.heap_lang Require Export locations.
-From iris.algebra Require Export ofe.
 From stdpp Require Export binders strings.
 From stdpp Require Import gmap.
+From iris.algebra Require Export ofe.
+From iris.program_logic Require Export language ectx_language ectxi_language.
+From iris.heap_lang Require Export locations.
 Set Default Proof Using "Type".
 
 (** heap_lang.  A fairly simple language used for common Iris examples.
diff --git a/theories/heap_lang/lib/arith.v b/theories/heap_lang/lib/arith.v
index 57f7c4fb3..bbaf8716d 100644
--- a/theories/heap_lang/lib/arith.v
+++ b/theories/heap_lang/lib/arith.v
@@ -1,6 +1,6 @@
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/theories/heap_lang/lib/assert.v b/theories/heap_lang/lib/assert.v
index 04a6d7613..b8c932ef1 100644
--- a/theories/heap_lang/lib/assert.v
+++ b/theories/heap_lang/lib/assert.v
@@ -1,6 +1,6 @@
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index 7fc424dd6..c62373138 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -1,8 +1,8 @@
-From iris.heap_lang Require Export lifting notation.
-From iris.program_logic Require Export atomic.
-From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation.
 From iris.bi.lib Require Import fractional.
+From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export atomic.
+From iris.heap_lang Require Export lifting notation.
+From iris.heap_lang Require Import proofmode.
 Set Default Proof Using "Type".
 
 (** A general logically atomic interface for a heap. *)
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 4b7058988..8dfe67e62 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -1,8 +1,8 @@
-From iris.program_logic Require Export weakestpre.
-From iris.base_logic.lib Require Export invariants.
-From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac_auth auth.
+From iris.base_logic.lib Require Export invariants.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/theories/heap_lang/lib/diverge.v b/theories/heap_lang/lib/diverge.v
index 38b00be2a..9f12d7234 100644
--- a/theories/heap_lang/lib/diverge.v
+++ b/theories/heap_lang/lib/diverge.v
@@ -1,6 +1,6 @@
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index 00065aa8d..ef86e1aef 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -1,8 +1,8 @@
+From iris.bi.lib Require Import fractional.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export atomic.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation atomic_heap par.
-From iris.bi.lib Require Import fractional.
 Set Default Proof Using "Type".
 
 (** Show that implementing fetch-and-add on top of CAS preserves logical
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index a5d9966a2..1bd35bf56 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -1,5 +1,5 @@
-From iris.heap_lang Require Export lifting notation.
 From iris.base_logic.lib Require Export invariants.
+From iris.heap_lang Require Export lifting notation.
 Set Default Proof Using "Type".
 
 Structure lock Σ `{!heapG Σ} := Lock {
@@ -36,4 +36,3 @@ Existing Instances is_lock_ne is_lock_persistent locked_timeless.
 
 Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N γ lk:
   Proper ((≡) ==> (≡)) (is_lock L N γ lk) := ne_proper _.
-
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 558853f4f..a9378e599 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -1,5 +1,5 @@
-From iris.heap_lang Require Export spawn.
 From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Export spawn.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 7e698d52b..5b78e389c 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -1,9 +1,9 @@
-From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl.
 From iris.base_logic.lib Require Export invariants.
+From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl.
 Set Default Proof Using "Type".
 
 Definition spawn : val :=
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 3370bdcc2..f0aab59b4 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -1,8 +1,8 @@
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl.
 From iris.heap_lang.lib Require Import lock.
 Set Default Proof Using "Type".
 
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 5600f18d9..8296258b6 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -1,8 +1,8 @@
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl auth gset.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl auth gset.
 From iris.heap_lang.lib Require Export lock.
 Set Default Proof Using "Type".
 Import uPred.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 5bfbac134..780a0eae4 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,3 +1,5 @@
+From stdpp Require Import fin_maps.
+From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
 From iris.base_logic Require Export gen_heap.
 From iris.base_logic.lib Require Export proph_map.
@@ -5,8 +7,6 @@ From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics notation.
-From iris.proofmode Require Import tactics.
-From stdpp Require Import fin_maps.
 Set Default Proof Using "Type".
 
 Class heapG Σ := HeapG {
diff --git a/theories/heap_lang/locations.v b/theories/heap_lang/locations.v
index 7484c98ab..4f4df7d12 100644
--- a/theories/heap_lang/locations.v
+++ b/theories/heap_lang/locations.v
@@ -1,5 +1,5 @@
-From iris.algebra Require Import base.
 From stdpp Require Import countable numbers gmap.
+From iris.algebra Require Import base.
 
 Record loc := { loc_car : Z }.
 
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 9df37184b..49629d63e 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -1,5 +1,5 @@
-From iris.heap_lang Require Export lang.
 From stdpp Require Import gmap.
+From iris.heap_lang Require Export lang.
 
 (* This file contains some metatheory about the heap_lang language,
   which is not needed for verifying programs. *)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index e65610e73..fc4913c1b 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -1,7 +1,7 @@
-From iris.program_logic Require Export weakestpre total_weakestpre.
-From iris.program_logic Require Import atomic.
 From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Export tactics.
+From iris.program_logic Require Export weakestpre total_weakestpre.
+From iris.program_logic Require Import atomic.
 From iris.heap_lang Require Export tactics lifting array.
 From iris.heap_lang Require Import notation.
 Set Default Proof Using "Type".
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index df83c1542..8c2f6ffb5 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -1,7 +1,7 @@
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export total_adequacy.
 From iris.heap_lang Require Export adequacy.
 From iris.heap_lang Require Import proofmode notation.
-From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 95d2a04ff..11961ee32 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -1,7 +1,7 @@
-From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic.lib Require Import wsat.
-From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 847f2705c..a8b7064b4 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -1,8 +1,8 @@
 From stdpp Require Import namespaces.
-From iris.program_logic Require Export weakestpre.
-From iris.proofmode Require Import tactics classes.
-From iris.bi.lib Require Export atomic.
 From iris.bi Require Import telescopes.
+From iris.bi.lib Require Export atomic.
+From iris.proofmode Require Import tactics classes.
+From iris.program_logic Require Export weakestpre.
 Set Default Proof Using "Type".
 
 (* This hard-codes the inner mask to be empty, because we have yet to find an
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index a164cb131..67d73d853 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -1,6 +1,6 @@
 (** Some derived lemmas for ectx-based languages *)
-From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export ectx_language weakestpre lifting.
 Set Default Proof Using "Type".
 
 Section wp.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index e2af2d5c1..3275afc7d 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -1,6 +1,6 @@
-From iris.program_logic Require Export weakestpre.
-From iris.base_logic.lib Require Export viewshifts.
 From iris.proofmode Require Import tactics.
+From iris.base_logic.lib Require Export viewshifts.
+From iris.program_logic Require Export weakestpre.
 Set Default Proof Using "Type".
 
 Definition ht `{!irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 3219b1456..f560a780b 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -1,5 +1,5 @@
-From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre.
 Set Default Proof Using "Type".
 
 Section lifting.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 40f4763f9..02af1aeef 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -1,8 +1,8 @@
+From iris.proofmode Require Import tactics classes.
+From iris.algebra Require Import excl auth.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
-From iris.algebra Require Import excl auth.
-From iris.proofmode Require Import tactics classes.
 Set Default Proof Using "Type".
 
 (**
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 7d5512c4c..1f8d68102 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -1,7 +1,7 @@
-From iris.program_logic Require Export total_weakestpre adequacy.
-From iris.algebra Require Import gmap auth agree gset coPset list.
 From iris.bi Require Import big_op fixpoint.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import gmap auth agree gset coPset list.
+From iris.program_logic Require Export total_weakestpre adequacy.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/program_logic/total_ectx_lifting.v b/theories/program_logic/total_ectx_lifting.v
index 3e1168bfc..9fe8e494e 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -1,7 +1,6 @@
 (** Some derived lemmas for ectx-based languages *)
-From iris.program_logic Require Export ectx_language.
-From iris.program_logic Require Export total_weakestpre total_lifting.
 From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export ectx_language total_weakestpre total_lifting.
 Set Default Proof Using "Type".
 
 Section wp.
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
index c2e7a9086..eaf71db02 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -1,6 +1,6 @@
-From iris.program_logic Require Export total_weakestpre.
 From iris.bi Require Export big_op.
 From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export total_weakestpre.
 Set Default Proof Using "Type".
 
 Section lifting.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 9ab29cf73..920d17d1e 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -1,6 +1,6 @@
-From iris.program_logic Require Export weakestpre.
-From iris.proofmode Require Import tactics.
 From iris.bi Require Import fixpoint big_op.
+From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index f7554040d..36575f35a 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -1,7 +1,9 @@
+From iris.proofmode Require Import base tactics classes.
 From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
+(* FIXME: If we import iris.bi.weakestpre earlier texan triples do not
+   get pretty-printed correctly. *)
 From iris.bi Require Export weakestpre.
-From iris.proofmode Require Import base tactics classes.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index a4b54719b..45e060b66 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -1,6 +1,6 @@
+From Coq Require Export Ascii.
 From stdpp Require Export strings.
 From iris.algebra Require Export base.
-From Coq Require Export Ascii.
 Set Default Proof Using "Type".
 
 (** * Utility definitions used by the proofmode *)
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 5362da96c..e8eeb5d9d 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -1,7 +1,7 @@
+From stdpp Require Import namespaces.
 From iris.bi Require Export bi.
 From iris.proofmode Require Import base.
 From iris.proofmode Require Export modalities.
-From stdpp Require Import namespaces.
 Set Default Proof Using "Type".
 Import bi.
 
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index f3e8e93f7..2ae03b1d5 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -1,7 +1,7 @@
-From iris.proofmode Require Import base.
-From iris.algebra Require Export base.
 From iris.bi Require Export bi.
 From iris.bi Require Import tactics.
+From iris.proofmode Require Import base.
+From iris.algebra Require Export base.
 Set Default Proof Using "Type".
 Import bi.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index b63077368..6f696ed02 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1,9 +1,8 @@
-From iris.proofmode Require Import coq_tactics reduction.
-From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
+From stdpp Require Import namespaces hlist pretty.
 From iris.bi Require Export bi telescopes.
-From stdpp Require Import namespaces.
+From iris.proofmode Require Import base intro_patterns spec_patterns
+                                   sel_patterns coq_tactics reduction.
 From iris.proofmode Require Export classes notation.
-From stdpp Require Import hlist pretty.
 Set Default Proof Using "Type".
 Export ident.
 
diff --git a/theories/proofmode/modalities.v b/theories/proofmode/modalities.v
index b5b9bcc0a..b4a5e0236 100644
--- a/theories/proofmode/modalities.v
+++ b/theories/proofmode/modalities.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export bi.
 From stdpp Require Import namespaces.
+From iris.bi Require Export bi.
 Set Default Proof Using "Type".
 Import bi.
 
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 03fb2f02b..f9a53fb58 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import coq_tactics environments.
 From stdpp Require Export strings.
+From iris.proofmode Require Import coq_tactics environments.
 Set Default Proof Using "Type".
 
 Delimit Scope proof_scope with env.
-- 
GitLab