diff --git a/ProofGuide.md b/ProofGuide.md
index af06f6ab36c80730d6bcfd87feb02b84e94d72f2..81fb498200900d22efc02a757c45d50053a24422 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 236ec1e71c6f641b70281fc407182ab11ac2d497..6e3b5707708c36a2c59723e04b74956901b3d132 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 f2e7050b08a79b9d03455054de061461006401a5..85dcae1bcf41917c66aa260815df078b66cb9a30 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 79ec0d82a344c5adb38d4b01c18b18cea2973f3e..d279aded7857a8d25a4a43db2b6509fcb0b6d3ee 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 95850a2d400a404f4447a11751d6c75fd0225d50..ba12c859905dd3f19d95dd96c063f2a6537d4798 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 25211740a8f9c6cf244641c542422e59dbe31abe..bb9eb5b427352468334f8ac270d7ba63e01a49df 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 dd9f08ed060ab562e79a19aee1753fe845ea1dea..03441f82772f02a2ec5cb5b267aaf43c67abb602 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 5aec754586506f53dda54a0c69b654ceda06ccc2..ee19d85814f75fa4d2a3e55400c8ea295424435d 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 c959fbf031f79d3ab127273173c7787d1d97a628..d7f1865a9444f75a39dfd962b5bc6f0a89f8a6c3 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 b2dad6a874ec382cffc2f47c45072e909fd4f7d9..ecd650d5817c583079f984d19fcbf7f237cc65f2 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 cb9109bfc48b4dfa0558e77dd76c21fed55444c6..fb4badc2390d4f0345be62f5b2acbe21fbeb9f5e 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 635bb926744c54f3872d50f0857699cd07e55e0d..8fbfcdddfa02c4574001230dd46b3e094507057c 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 6bbf5244d71c79146708ff33582370f8234cf1bf..65467b604ca0ca07055f740d49d6fd66fbfbc621 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 326c0251dd2f0ac1123038d67b4ec2378e3695e9..0cae57b57d96f71b44334bfa34b3e2e92379b403 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 2749d4ec857cefa69e347b2018ceaa29a1f1a52b..86d121530b3324068869965191cdac31736212d8 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 3f7d27c3cdcdd5066af33f9240ec3abafcfe715f..46d1e180d89c88235ceacca382f1c1050b1cdf08 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 3e66c877b8d091658989405848a03a337687daab..80e65d794a6c49f6b076e39f3e3e1e8bf3c28c13 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 38fb0a48a19c329eb3ba5ce6efb0f53cf1faa98a..021184995f8e095853db0f7ff389b4fff3170762 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 bd463713475cc7e0bfbbdcb600de60d61f4d627a..7572718e9d9d33c329fa10e733eb7a77974a932d 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 b0b7fc5121f062bb799434d4978f9f6951b9d646..14773b60ed3a52f2265cf7fb0f9e026ba498b3dd 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 d97f640aabf04d14d62757d8c41fb9a829f3e110..e89df5de08ac39fc18cd5a78579d03bb0aa3e508 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 93c2ff11755541bd73630f61c0ed5e7799a44d4a..72949d1b2c6fc41ca5f2fc53b0fccc73a3e5a0f8 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 7ccebbe786a091147778f9ca798f9ab62a8b84a0..c87bc6fa2809eb5c32a872b27235eb4c74938276 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 cec6d972f60f3a69d8193fd0d096cd44f625eae7..af7a5c07faf71310695462626944aa9fbfedede7 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 5059f6575fa7f53f83a3c406545d7ea703a88aca..13c4da99453751133025fb27e4f4fbaab2916bb2 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 11a1a6a4032883379eb8edc3a8bc861a95b81c69..7c86fd444fc956ce69687275e6f47c3bac590653 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 9cc3208a990027a434ec535e9456bf2b827b894e..67d04dc7aa32c1736f9fe9aca047bf2c6aab87d4 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 0adcc1a5c714ad87056f98e924db35bacaec7877..3c9527a6fb280a8f7a0968d58d8442cdeb39e4a1 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 c5a8b494a3e540ae9e5ee66c339da83fc6571ad4..0d754209f7303cc2554f0e785898e7b103cb839a 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 7de8683962f869d789e4a89b50e701fce44241cd..1aa38e78b917db6e67532236d7bbc05b06ba7a5e 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 78288c7e08ebd9fd2dc521eab426f6cb1d3af7ed..9fe5817595fef20e659ee7561579ddc50a74eddb 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 6dfaa0d0c3a4fa48a50287bc15751e36b22f12db..024f6410ae410a3aa49bed4bdcd193e6c5b7a33d 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 b47fa0df6b8b48693d4c8baf4df9ede3836f884e..a5c376e163eb76c3fae34bee4c2ccc2d331456bf 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 18ba74aba4a86a656a88a0e3250a9646b7a2f436..6a3c44d0b5fa332c9a38c80438fad5b1010b1a2f 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 cadd6f23126e056083bc2b25ef879546657e7eef..b00b422411ae73adf1eca465593e078d60f70f9b 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 809bfe6409449898a8fd393ec71652509825f76f..269b15c9becbc780512a24ea3a8f6868435566b4 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 680d3429535dcc2d90ea6cebd8bc22bef8117a30..eff3c4abc521d9c22be852ddd5df3ff373b23097 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 822b32f30330798256bdd1240fb75abd38ad84dd..ba33ca2f39a57568e0de66691b139b9c8bf4c2c4 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 28962d6cb847994872931281ec300323e14fd12b..4891e0b9efb0ef8d598de43ace3edf44b6fe8c4b 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 2af2c2712b171376218f3f8f27131dceac20591b..af76fb78931245935cc85f798fdf2a26b0278f29 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 6004e1b4bb4d4d54fd25f42b6d862a2e57364da8..ad55707f2192ada2f8fb50538395cd417562a537 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 a727317d2af5ab0bf82a69e1de6e9e6da7c9cc8f..5fe481ad4e9d12f28bbdf42319e525c34196462b 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 6ffb41ff725616ab7e44b9e07fae6ac257635f84..1c380e86deaa4cd53b63d3cfb51caa5d5efb1f5f 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 944b92e84cc49158e830d63ffbef3fdf2f6d2ed6..c5eba535ba9adb7204f53152895027ab453fa1c6 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 b861d2284d29cffe1db9c0363b6cad57bab70679..b2bf5f05ce1a1370d2ed08bdd05ba57d072120e6 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 6120bf009339f98b4176f8285baf1c2e19aa0e93..e938f99eb6e3be9ead8a7027a481bb523f61aea0 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 2410b808b75581e115f6bef5f54d57965b63c73e..cd9fe751cd0b9f1e27f8485f8984006a847577ff 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 3d3ea3b860ff401c580599f2f18074f3f8b8e6bc..4eb80f6c79b4ab114300d79bb226b66cf1d93ad9 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 bcfc613bc11b66dbe7ba73c3a08c3e23d57d5f16..a66e00c3b811bb70dd1a57b7ee415144b5e7dbb7 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 387b24bf8d789e3f0d09910a85b943dcc9333e24..d6de4370c2a4a6ea5f86b0afbf25f4c91a2cfa6e 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 d3b20324a43c4ab9fac2cb3fb95aeed67bf7be80..da8ba0adc49d65d1e8368af3b0bf72efdb525020 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 15331b9e8f1cd5f3726207ab93a69dcef1907f14..31d63f27bf63767880dc4f66b18b98c1a2643c83 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 4371dc2376a72e4d96c9d61074697781eaeefe3c..4a99a3c32799a5b2f569bc6d968ea0ccfcc5d4b8 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 57f7c4fb313411febc8330c11e5e950fb328d4a0..bbaf8716d60ae9b68466d0a3fab641f32a191623 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 04a6d76133fb524c6e9e99961af2524ad50bd4de..b8c932ef13879b50dfcca1eb5a44895194718dc4 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 7fc424dd67486bde7a7e6c02c0eb92fb3044deb6..c6237313879a237b115f98c98a7a83e62d26843c 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 4b7058988290aa68957ca306c2dfbbf50ef5030a..8dfe67e62b8a32288ec934ecf405a0447ea8d6da 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 38b00be2a81578ee6c20bba006c5c83465236d7a..9f12d72347d286bae01bf3024ddde255e122f2e5 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 00065aa8db13d86a5800827e900acf787c7604ef..ef86e1aef8595ee6c042c5aaf36b5a402d0833fc 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 a5d9966a25060e0ffdd20dc6bc361e9bf7ee8dae..1bd35bf56ea661b99240d01eeff0dee87739a9f8 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 558853f4f48d15d4eae8f61cffd88981686e4abd..a9378e5992195b885a57c06ea5706f16e36e5fbc 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 7e698d52bbe39eb5b94ee5c18be0986285120d36..5b78e389c96b194c94e975f55b19d01ce4982d79 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 3370bdcc298b5bb75baf9bcadd318512c61d9ca1..f0aab59b4d1bec01bcbc8cf1f3d7010dad81db56 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 5600f18d9fd5495eb91bbe97dd9723755b8dfdcf..8296258b676ba98bded79e7d42069bc1bb72abac 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 5bfbac13480d928fc6140f36b049579ee5bb838f..780a0eae4f3fbb2d11ef69478fa7c9c68fe95128 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 7484c98ab8e5870ca92fe0992009c0586d9fdd7c..4f4df7d122ea161f19aec98e2e071dbc5b3f5cc9 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 9df37184bacf13d0a4d26fa7f33a4967e6d467ef..49629d63e946fb8a4d23eabc33131e4df1755dfb 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 e65610e737126e588bf5aeca17307bb75ee76216..fc4913c1bcc81d016f23c6e229bbc7a19cbdfc55 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 df83c1542262baae6879521cf1110864640ee607..8c2f6ffb5b9d91cbc838bf4a01545bb681bf4972 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 95d2a04ff73b35eaec1ebe6ca7af5aaddd27fb70..11961ee328e16fe4ea265976451e07e8396d25df 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 847f2705c4e62060a7deda32e7ee79a3476eec51..a8b7064b41a799e503b1b64f47561921e93ea5dd 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 a164cb131c7094b1577c1284b296eab7c60ad42f..67d73d853d1572e8d998ac93aa7bcad1de6768f4 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 e2af2d5c1574b974a0ea0cf57d7a19ff1ef8ab5f..3275afc7dbfe9084a9b9f17e207388a0e0855571 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 3219b14562eebf13e43e3b30f9b20a44c8b43230..f560a780b5af63be602ad34261136abdb96a2ddb 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 40f4763f94dd1f05d7895876f7aeb87d4dd9b1f3..02af1aeefea82e0f5558b74058d6fa85fa3173b7 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 7d5512c4cd4fb38836bd811af0fd20b2f08e3ef4..1f8d68102ef5d7e7898b208da88d424402a4684e 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 3e1168bfcc0d6b725e691b603856dfd91e195fd0..9fe8e494e0933034cf83b705b770773f2579d324 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 c2e7a9086c0da1dd55d196e791c494c20c41a5e6..eaf71db025ebc7016290dc2fa54b8fe52880ea10 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 9ab29cf73e84b91398d9090e775206a8a7d20f35..920d17d1e735120fa5b368f465de7d17be42cbab 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 f7554040da8d67298776ac384f127c6ffb9c0b68..36575f35a3bc707556c7770e4886ebed8cba6936 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 a4b54719b1069e0c9cdfd456d3e2433a2e851d0c..45e060b66f44a77b7d64e23256b9f36f4cfbe273 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 5362da96ce875de8917c3f398f124cfb769898ef..e8eeb5d9da56f44697da48beba3ab41c62fd0236 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 f3e8e93f7fca2a6b4992f520f110a5f2ccfa78ed..2ae03b1d5b9ef51b6a87a6449365a8bbff21f314 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 b63077368563de53cf2796056b845bc73edaabe1..6f696ed02a5841d8feecbf92ad4247929e931933 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 b5b9bcc0a361cbe88704f343ce1a7956a8559676..b4a5e0236ef6cc4d0001073bdaa3fa90f6b92418 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 03fb2f02b03a781a6aef990515e3cb46956c3304..f9a53fb58c747793bc5d38d551e6bc8b2c359789 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.