fix import ordering

tests/one_shot.v

-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl agree csum.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.

tests/one_shot_once.v

-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac agree csum.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.

tests/proofmode_iris.v

-From iris.proofmode Require Import tactics monpred.
 From iris.algebra Require Import frac.
+From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 

theories/base_logic/derived.v

-From iris.bi Require Export bi.
 From iris.algebra Require Import frac.
+From iris.bi Require Export bi.
 From iris.base_logic Require Export bi.
 From iris Require Import options.
 Import bi.bi base_logic.bi.uPred.

theories/base_logic/lib/auth.v

-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.
 From iris Require Import options.
 Import uPred.

theories/base_logic/lib/boxes.v

-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import lib.excl_auth gmap agree.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.

theories/base_logic/lib/cancelable_invariants.v

+From iris.algebra Require Export frac.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Export frac.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.

theories/base_logic/lib/fancy_updates.v

 From stdpp Require Export coPset.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import wsat.
 From iris Require Import options.

theories/base_logic/lib/gen_heap.v

 From stdpp Require Export namespaces.
+From iris.algebra Require Import gmap_view namespace_map agree frac.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import gmap_view namespace_map agree frac.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 Import uPred.

theories/base_logic/lib/ghost_var.v

 (** A simple "ghost variable" of arbitrary type with fractional ownership.
 Can be mutated when fully owned. *)
+From iris.algebra Require Import frac_agree.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import frac_agree.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 

theories/base_logic/lib/invariants.v

 From stdpp Require Export namespaces.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export fancy_updates.
 From iris.base_logic.lib Require Import wsat.
 From iris Require Import options.

theories/base_logic/lib/mnat.v

@@ -8,9 +8,9 @@ lower-bound at [m] imply that [m ≤ n], and [mnat_update], which allows to
 increase the auth element. At any time the auth nat can be "snapshotted" with
 [mnat_get_lb] to produce a persistent lower-bound proposition. *)
 
-From iris.proofmode Require Import tactics.
 From iris.algebra.lib Require Import mnat_auth.
 From iris.bi.lib Require Import fractional.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 

theories/base_logic/lib/na_invariants.v

-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gset coPset.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.

theories/base_logic/lib/saved_prop.v

 From stdpp Require Import gmap.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import agree.
+From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export own.
 From iris Require Import options.
 Import uPred.

theories/base_logic/lib/sts.v

-From iris.proofmode Require Import tactics.
 From iris.algebra Require Export sts.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris Require Import options.
 Import uPred.

theories/base_logic/lib/wsat.v

 From stdpp Require Export coPset.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap_view gset coPset.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 

theories/base_logic/upred.v

 From stdpp Require Import finite.
-From iris.bi Require Import notation.
 From iris.algebra Require Export cmra updates.
+From iris.bi Require Import notation.
 From iris Require Import options.
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|] : core.
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption] : core.

theories/bi/ascii.v

 From iris.bi Require Import interface derived_connectives updates.
-From iris.algebra Require Export ofe.
 From iris Require Import options.
 
 Notation "P |- Q" := (P ⊢ Q)

theories/bi/derived_connectives.v

-From iris.bi Require Export interface.
 From iris.algebra Require Import monoid.
+From iris.bi Require Export interface.
 From iris Require Import options.
 
 Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.

theories/bi/derived_laws.v

-From iris.bi Require Export derived_connectives.
 From iris.algebra Require Import monoid.
+From iris.bi Require Export derived_connectives.
 From iris Require Import options.
 
 (* The sections add [BiAffine] and the like, which is only picked up with [Type*]. *)