From c48296a0a9cbb59ddcff2f80eeb6e96b9375e36f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Nov 2020 10:26:11 +0100
Subject: [PATCH] fix import ordering

---
 tests/one_shot.v                                | 2 +-
 tests/one_shot_once.v                           | 2 +-
 tests/proofmode_iris.v                          | 2 +-
 theories/base_logic/derived.v                   | 2 +-
 theories/base_logic/lib/auth.v                  | 2 +-
 theories/base_logic/lib/boxes.v                 | 2 +-
 theories/base_logic/lib/cancelable_invariants.v | 2 +-
 theories/base_logic/lib/fancy_updates.v         | 2 +-
 theories/base_logic/lib/gen_heap.v              | 2 +-
 theories/base_logic/lib/ghost_var.v             | 2 +-
 theories/base_logic/lib/invariants.v            | 2 +-
 theories/base_logic/lib/mnat.v                  | 2 +-
 theories/base_logic/lib/na_invariants.v         | 2 +-
 theories/base_logic/lib/saved_prop.v            | 2 +-
 theories/base_logic/lib/sts.v                   | 2 +-
 theories/base_logic/lib/wsat.v                  | 2 +-
 theories/base_logic/upred.v                     | 2 +-
 theories/bi/ascii.v                             | 1 -
 theories/bi/derived_connectives.v               | 2 +-
 theories/bi/derived_laws.v                      | 2 +-
 theories/bi/derived_laws_later.v                | 2 +-
 theories/bi/embedding.v                         | 2 +-
 theories/bi/interface.v                         | 2 +-
 theories/bi/plainly.v                           | 2 +-
 theories/heap_lang/adequacy.v                   | 2 +-
 theories/heap_lang/lib/counter.v                | 2 +-
 theories/heap_lang/lib/spawn.v                  | 2 +-
 theories/heap_lang/lib/spin_lock.v              | 2 +-
 theories/heap_lang/lib/ticket_lock.v            | 2 +-
 theories/heap_lang/primitive_laws.v             | 2 +-
 theories/program_logic/adequacy.v               | 2 +-
 theories/program_logic/ownp.v                   | 2 +-
 theories/program_logic/total_adequacy.v         | 2 +-
 theories/proofmode/environments.v               | 2 +-
 34 files changed, 33 insertions(+), 34 deletions(-)

diff --git a/tests/one_shot.v b/tests/one_shot.v
index 13b4e05aa..3de778074 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -1,5 +1,5 @@
-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.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 40efb5efc..13230b728 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -1,5 +1,5 @@
-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.
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index a01fafc46..96b2f643a 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -1,5 +1,5 @@
-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.
 
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 3bcb256e3..334000233 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,5 +1,5 @@
-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.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index d02ce5306..2d99ad3c1 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -1,6 +1,6 @@
-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.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index a186d80b6..179153fb4 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -1,5 +1,5 @@
-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.
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index f0b3719da..1c8964fc3 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -1,6 +1,6 @@
+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.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index ccd4ac39c..558fae055 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -1,6 +1,6 @@
 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.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index ac6140a66..b48e4b052 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -1,7 +1,7 @@
 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.
diff --git a/theories/base_logic/lib/ghost_var.v b/theories/base_logic/lib/ghost_var.v
index 0632b0c24..49aba300b 100644
--- a/theories/base_logic/lib/ghost_var.v
+++ b/theories/base_logic/lib/ghost_var.v
@@ -1,8 +1,8 @@
 (** 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.
 
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index adff4f6eb..5fa9cd8d0 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -1,6 +1,6 @@
 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.
diff --git a/theories/base_logic/lib/mnat.v b/theories/base_logic/lib/mnat.v
index 9773e4faf..36096f2bf 100644
--- a/theories/base_logic/lib/mnat.v
+++ b/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.
 
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index c99198241..65bb13da8 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -1,5 +1,5 @@
-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.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 586725300..f9915ee2b 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -1,6 +1,6 @@
 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.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 30ceaa110..329ead42a 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -1,5 +1,5 @@
-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.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 020d584ae..c64dcebcd 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -1,6 +1,6 @@
 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.
 
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 8b443a61b..1508ddcc1 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,6 +1,6 @@
 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.
diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 52ec4bebf..434592fd9 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -1,5 +1,4 @@
 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)
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index fdeb3a982..671a8ae13 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -1,5 +1,5 @@
-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.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 5227d08ed..7941169a2 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1,5 +1,5 @@
-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*]. *)
diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index a683467de..03d950b19 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export derived_laws.
 From iris.algebra Require Import monoid.
+From iris.bi Require Export derived_laws.
 From iris Require Import options.
 
 Module bi.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 4a70ddb3b..bb73cf16a 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,6 +1,6 @@
+From iris.algebra Require Import monoid.
 From iris.bi Require Import interface derived_laws_later big_op.
 From iris.bi Require Import plainly updates internal_eq.
-From iris.algebra Require Import monoid.
 From iris Require Import options.
 
 (* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index ba41b1898..dc7155fb2 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,5 +1,5 @@
-From iris.bi Require Export notation.
 From iris.algebra Require Export ofe.
+From iris.bi Require Export notation.
 From iris Require Import options.
 Set Primitive Projections.
 
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 756dba593..29ee3437d 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,5 +1,5 @@
-From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris.algebra Require Import monoid.
+From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 7ffc5a931..1c6666270 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Import proofmode notation.
 From iris Require Import options.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 72109448c..48537d024 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import lib.frac_auth numbers auth.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 9b10f9247..0d033c5d1 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
+From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 1e5af4e73..8f4986496 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 850db347d..5b202eaed 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl auth gset.
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index afb76b7db..5e1ccb1e6 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -2,8 +2,8 @@
 the Iris lifting lemmas. *)
 
 From stdpp Require Import fin_maps.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
+From iris.proofmode Require Import tactics.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Export gen_heap proph_map gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index fc3abc68c..309857a21 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -1,5 +1,5 @@
-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 Import wsat.
 From iris.program_logic Require Export weakestpre.
 From iris Require Import options.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 2a0fde9be..78e6ffcf9 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -1,5 +1,5 @@
-From iris.proofmode Require Import tactics classes.
 From iris.algebra Require Import lib.excl_auth.
+From iris.proofmode Require Import tactics classes.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 731f69079..1825b3cd9 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -1,6 +1,6 @@
+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.
 From iris Require Import options.
 Import uPred.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index b37062dc8..e77b6b44e 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -1,6 +1,6 @@
+From iris.algebra Require Export base.
 From iris.bi Require Export bi.
 From iris.proofmode Require Import base.
-From iris.algebra Require Export base.
 From iris Require Import options.
 Import bi.
 
-- 
GitLab