From 354c8da0638edea5a7fe4e91672f103c9153cea0 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Fri, 20 Oct 2023 20:21:41 +0200
Subject: [PATCH] consistently use From-Require

---
 core/DupDropReordering.v              |  1 +
 core/DynamicNetLemmas.v               | 14 +++++---------
 core/GhostSimulations.v               | 15 +++++----------
 core/HandlerMonad.v                   |  3 ++-
 core/InverseTraceRelations.v          |  7 +++----
 core/LabeledNet.v                     |  8 +++-----
 core/NameOverlay.v                    |  9 ++++-----
 core/Net.v                            | 20 +++++++-------------
 core/PartialExtendedMapSimulations.v  | 15 +++++----------
 core/PartialMapExecutionSimulations.v | 21 +++++++--------------
 core/PartialMapSimulations.v          | 15 +++++----------
 core/SingleSimulations.v              |  6 ++----
 core/StateMachineHandlerMonad.v       |  2 +-
 core/StatePacketPacketDecomposition.v |  8 +-------
 core/TotalMapExecutionSimulations.v   | 15 ++++-----------
 core/TotalMapSimulations.v            | 12 ++++--------
 core/TraceRelations.v                 |  8 ++++----
 core/Verdi.v                          | 20 +++++++-------------
 core/VerdiHints.v                     |  8 +++-----
 extraction/ExtrOcamlBasicExt.v        |  2 +-
 extraction/ExtrOcamlBool.v            |  4 ++--
 extraction/ExtrOcamlDiskOp.v          |  4 ++--
 extraction/ExtrOcamlFinInt.v          |  4 ++--
 extraction/ExtrOcamlList.v            |  4 ++--
 extraction/ExtrOcamlNatIntExt.v       |  5 ++---
 lib/FMapVeryWeak.v                    | 22 +++++++---------------
 lib/Ssrexport.v                       |  6 +++---
 systems/Counter.v                     |  3 +--
 systems/LockServ.v                    |  8 +++-----
 systems/LockServSeqNum.v              |  8 +++-----
 systems/Log.v                         |  5 ++---
 systems/LogCorrect.v                  |  9 ++++-----
 systems/SeqNum.v                      |  2 +-
 systems/SerializedMsgParams.v         |  5 +++--
 systems/SerializedMsgParamsCorrect.v  | 19 +++++++------------
 systems/VarD.v                        | 10 +++-------
 systems/VarDPrimaryBackup.v           |  9 +++------
 37 files changed, 124 insertions(+), 212 deletions(-)

diff --git a/core/DupDropReordering.v b/core/DupDropReordering.v
index 590e63db..4fd55b86 100644
--- a/core/DupDropReordering.v
+++ b/core/DupDropReordering.v
@@ -1,6 +1,7 @@
 From Coq Require Import List Relations Permutation.
 From StructTact Require Import StructTactics.
 From Verdi Require Import Net.
+
 Import ListNotations.
 
 Section dup_drop_reorder.
diff --git a/core/DynamicNetLemmas.v b/core/DynamicNetLemmas.v
index 56449f86..fc6d7054 100644
--- a/core/DynamicNetLemmas.v
+++ b/core/DynamicNetLemmas.v
@@ -1,12 +1,8 @@
-Require Import Verdi.Verdi.
-
-Require Import StructTact.Update.
-Require Import FunctionalExtensionality.
-Require Import Sumbool.
-Require Import Relation_Definitions.
-Require Import RelationClasses.
-
-Require Import Verdi.Ssrexport.
+From Verdi Require Import Verdi.
+From StructTact Require Import Update.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import Sumbool Relation_Definitions RelationClasses.
+From Verdi Require Import Ssrexport.
 
 Set Implicit Arguments.
 
diff --git a/core/GhostSimulations.v b/core/GhostSimulations.v
index 38fcd88d..69e766b6 100644
--- a/core/GhostSimulations.v
+++ b/core/GhostSimulations.v
@@ -1,13 +1,8 @@
-Require Import List.
-
-Require Import StructTact.StructTactics.
-Require Import Verdi.Net.
-Require Import StructTact.Util.
-
-Require Import FunctionalExtensionality.
-Require Import Verdi.TotalMapSimulations.
-
-Require Import Verdi.Ssrexport.
+From Coq Require Import List.
+From StructTact Require Import StructTactics Util.
+From Verdi Require Import Net TotalMapSimulations.
+From Coq Require Import FunctionalExtensionality.
+From Verdi Require Import Ssrexport.
 
 Set Implicit Arguments.
 
diff --git a/core/HandlerMonad.v b/core/HandlerMonad.v
index 6b4f316c..0749350a 100644
--- a/core/HandlerMonad.v
+++ b/core/HandlerMonad.v
@@ -1,4 +1,5 @@
-Require Import List.
+From Coq Require Import List.
+
 Import ListNotations.
 
 Definition GenHandler (W S O A : Type) : Type := S -> A * list O * S * list W % type.
diff --git a/core/InverseTraceRelations.v b/core/InverseTraceRelations.v
index 2f3dcb61..b4bfe308 100644
--- a/core/InverseTraceRelations.v
+++ b/core/InverseTraceRelations.v
@@ -1,7 +1,6 @@
-Require Import List.
-
-Require Import Verdi.Net.
-Require Import StructTact.StructTactics.
+From Coq Require Import List.
+From Verdi Require Import Net.
+From StructTact Require Import StructTactics.
 
 Class InverseTraceRelation `{State : Type} `{Event : Type} (step : step_relation State Event) :=
   {
diff --git a/core/LabeledNet.v b/core/LabeledNet.v
index 196da1a3..8f5d1bd2 100644
--- a/core/LabeledNet.v
+++ b/core/LabeledNet.v
@@ -1,8 +1,6 @@
-Require Import Verdi.Verdi.
-Require Import InfSeqExt.infseq.
-Require Import InfSeqExt.exteq.
-
-Require Import Verdi.Ssrexport.
+From Verdi Require Import Verdi.
+From InfSeqExt Require Import infseq exteq.
+From Verdi Require Import Ssrexport.
 
 Set Implicit Arguments.
 
diff --git a/core/NameOverlay.v b/core/NameOverlay.v
index fd6b4def..ae326e5d 100644
--- a/core/NameOverlay.v
+++ b/core/NameOverlay.v
@@ -1,7 +1,6 @@
-Require Import Verdi.Verdi.
-Require Import StructTact.Fin.
-
-Require Import OrderedType.
+From Verdi Require Import Verdi.
+From StructTact Require Import Fin.
+From Coq Require Import OrderedType.
 
 Module Type NameType.
   Parameter name : Type.
@@ -42,7 +41,7 @@ End NameOrderedTypeCompat.
 
 Module FinNameOrderedTypeCompat (N : NatValue) (FN : FinNameType N) <: NameOrderedTypeCompat FN := fin_OT_compat N.
 
-Require Import MSetInterface.
+From Coq Require Import MSetInterface.
 
 Module Type NameOrderedType (Import NT : NameType) <: OrderedType.
   Definition t := name.
diff --git a/core/Net.v b/core/Net.v
index 90a0f6c1..bae06d97 100644
--- a/core/Net.v
+++ b/core/Net.v
@@ -1,17 +1,11 @@
-Require Import List.
-Import ListNotations.
-
-Require Import StructTact.StructTactics.
-Require Import StructTact.Update.
-Require Import StructTact.Update2.
-Require Import StructTact.RemoveAll.
-Require Import Sumbool.
-Require Import Relation_Definitions.
-Require Import RelationClasses.
+From Coq Require Import List.
+From StructTact Require Import StructTactics.
+From StructTact Require Import Update Update2 RemoveAll.
+From Coq Require Import Sumbool Relation_Definitions RelationClasses.
+From Verdi Require Export VerdiHints.
+From Cheerios Require Import Cheerios.
 
-Require Export Verdi.VerdiHints.
-
-Require Import Cheerios.Cheerios.
+Import ListNotations.
 
 Set Implicit Arguments.
 
diff --git a/core/PartialExtendedMapSimulations.v b/core/PartialExtendedMapSimulations.v
index 55a8bddc..c24cd8d7 100644
--- a/core/PartialExtendedMapSimulations.v
+++ b/core/PartialExtendedMapSimulations.v
@@ -1,16 +1,11 @@
-Require Import Verdi.Verdi.
-Require Import Verdi.DynamicNetLemmas.
-Require Import Verdi.TotalMapSimulations.
-Require Import Verdi.PartialMapSimulations.
+From Verdi Require Import Verdi DynamicNetLemmas.
+From Verdi Require Import TotalMapSimulations PartialMapSimulations.
+From Coq Require Import FunctionalExtensionality Sumbool.
+From Coq Require Import Sorting.Permutation.
+From Verdi Require Import Ssrexport.
 
 Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
-Require Import FunctionalExtensionality.
-Require Import Sumbool.
-Require Import Sorting.Permutation.
-
-Require Import Verdi.Ssrexport.
-
 Set Implicit Arguments.
 
 Class MultiParamsPartialExtendedMap
diff --git a/core/PartialMapExecutionSimulations.v b/core/PartialMapExecutionSimulations.v
index ff31aae8..af33359a 100644
--- a/core/PartialMapExecutionSimulations.v
+++ b/core/PartialMapExecutionSimulations.v
@@ -1,20 +1,13 @@
-Require Import Verdi.Verdi.
-Require Import Verdi.LabeledNet.
-Require Import Verdi.TotalMapSimulations.
-Require Import Verdi.PartialMapSimulations.
-Require Import Verdi.TotalMapExecutionSimulations.
-
-Require Import InfSeqExt.infseq.
-Require Import InfSeqExt.map.
-Require Import InfSeqExt.exteq.
-
-Require Import FunctionalExtensionality.
+From Verdi Require Import Verdi LabeledNet.
+From Verdi Require Import TotalMapSimulations PartialMapSimulations.
+From Verdi Require Import TotalMapExecutionSimulations.
+From InfSeqExt Require Import infseq map exteq.
+From Coq Require Import FunctionalExtensionality.
+From Verdi Require Import Ssrexport.
+From Coq Require Import ssrbool.
 
 Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
-Require Import Verdi.Ssrexport.
-Require Import ssr.ssrbool.
-
 Set Implicit Arguments.
 
 Class LabeledMultiParamsPartialMapCongruency
diff --git a/core/PartialMapSimulations.v b/core/PartialMapSimulations.v
index e9a740ac..e10dfba3 100644
--- a/core/PartialMapSimulations.v
+++ b/core/PartialMapSimulations.v
@@ -1,16 +1,11 @@
-Require Import Verdi.Verdi.
-Require Import Verdi.DynamicNetLemmas.
-Require Import Verdi.TotalMapSimulations.
+From Verdi Require Import Verdi DynamicNetLemmas TotalMapSimulations.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import Sumbool Sorting.Permutation.
+From Verdi Require Import DynamicNetLemmas.
+From Verdi Require Import Ssrexport.
 
 Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
-Require Import FunctionalExtensionality.
-Require Import Sumbool.
-Require Import Sorting.Permutation.
-Require Import Verdi.DynamicNetLemmas.
-
-Require Import Verdi.Ssrexport.
-
 Set Implicit Arguments.
 
 Class BaseParamsPartialMap (P0 : BaseParams) (P1 : BaseParams) := 
diff --git a/core/SingleSimulations.v b/core/SingleSimulations.v
index 3a6099fb..c2be7bac 100644
--- a/core/SingleSimulations.v
+++ b/core/SingleSimulations.v
@@ -1,7 +1,5 @@
-Require Import Verdi.Verdi.
-Require Import Verdi.DynamicNetLemmas.
-
-Require Import Verdi.Ssrexport.
+From Verdi Require Import Verdi DynamicNetLemmas.
+From Verdi Require Import Ssrexport.
 
 Set Implicit Arguments.
 
diff --git a/core/StateMachineHandlerMonad.v b/core/StateMachineHandlerMonad.v
index 5895d7b8..b43b65dd 100644
--- a/core/StateMachineHandlerMonad.v
+++ b/core/StateMachineHandlerMonad.v
@@ -1,4 +1,4 @@
-Require Import List.
+From Coq Require Import List.
 
 (*
 This file is very similar to HandlerMonad.v, but supports step_1
diff --git a/core/StatePacketPacketDecomposition.v b/core/StatePacketPacketDecomposition.v
index a8f999ce..7ecd872d 100644
--- a/core/StatePacketPacketDecomposition.v
+++ b/core/StatePacketPacketDecomposition.v
@@ -1,4 +1,4 @@
-Require Import Verdi.Verdi.
+From Verdi Require Import Verdi.
 
 Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
@@ -101,12 +101,6 @@ Class Decomposition (B : BaseParams) (M : MultiParams B) :=
 Section Decomposition.
   Context `{d : Decomposition}.
 
-  (* Fixpoint remove_one {A : Type} (A_eq_dec : forall x y : A, {x = y} + {x <> y}) a l :=
-    match l with
-      | x :: xs => if A_eq_dec a x then xs else x :: remove_one A_eq_dec a xs
-      | [] => []
-    end. *)
-
   Definition packet_eq_dec :
     forall p1 p2 : packet,
       {p1 = p2} + {p1 <> p2}.
diff --git a/core/TotalMapExecutionSimulations.v b/core/TotalMapExecutionSimulations.v
index fc231943..036b64b2 100644
--- a/core/TotalMapExecutionSimulations.v
+++ b/core/TotalMapExecutionSimulations.v
@@ -1,17 +1,10 @@
-Require Import Verdi.Verdi.
-Require Import Verdi.LabeledNet.
-Require Import Verdi.TotalMapSimulations.
-
-Require Import InfSeqExt.infseq.
-Require Import InfSeqExt.map.
-Require Import InfSeqExt.exteq.
-
-Require Import FunctionalExtensionality.
+From Verdi Require Import Verdi LabeledNet TotalMapSimulations.
+From InfSeqExt Require Import infseq map exteq.
+From Coq Require Import FunctionalExtensionality.
+From Verdi Require Import Ssrexport.
 
 Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
-Require Import Verdi.Ssrexport.
-
 Set Implicit Arguments.
 
 Class LabeledMultiParamsLabelTotalMap
diff --git a/core/TotalMapSimulations.v b/core/TotalMapSimulations.v
index 4da74f61..f63749b2 100644
--- a/core/TotalMapSimulations.v
+++ b/core/TotalMapSimulations.v
@@ -1,14 +1,10 @@
-Require Import Verdi.Verdi.
-Require Import Verdi.DynamicNetLemmas.
+From Verdi Require Import Verdi DynamicNetLemmas.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import Sorting.Permutation Sumbool.
+From Verdi Require Import Ssrexport.
 
 Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
-Require Import FunctionalExtensionality.
-Require Import Sorting.Permutation.
-Require Import Sumbool.
-
-Require Import Verdi.Ssrexport.
-
 Set Implicit Arguments.
 
 Class BaseParamsTotalMap (P0 : BaseParams) (P1 : BaseParams) :=
diff --git a/core/TraceRelations.v b/core/TraceRelations.v
index 7b349cba..72b337db 100644
--- a/core/TraceRelations.v
+++ b/core/TraceRelations.v
@@ -1,8 +1,8 @@
-Require Import List.
-Import ListNotations.
+From Coq Require Import List.
+From Verdi Require Import Net.
+From StructTact Require Import StructTactics.
 
-Require Import Verdi.Net.
-Require Import StructTact.StructTactics.
+Import ListNotations.
 
 Class TraceRelation `{State : Type} `{Event : Type} (step : step_relation State Event) :=
   {
diff --git a/core/Verdi.v b/core/Verdi.v
index 73dcc63e..7964aa55 100644
--- a/core/Verdi.v
+++ b/core/Verdi.v
@@ -1,14 +1,8 @@
-Require Export List.
+From Coq Require Export List.
 Export ListNotations.
-Require Export Arith.
-Require Export Lia.
-Require Export Coq.Numbers.Natural.Abstract.NDiv.
-Require Export Sorting.Permutation.
-
-Require Export StructTact.Util.
-Require Export StructTact.StructTactics.
-
-Require Export Verdi.VerdiHints.
-Require Export Verdi.Net.
-
-Require PeanoNat.
+From Coq Require Export Arith Lia.
+From Coq Require Export Numbers.Natural.Abstract.NDiv.
+From Coq Require Export Sorting.Permutation.
+From StructTact Require Export Util StructTactics.
+From Verdi Require Export VerdiHints Net.
+From Coq Require PeanoNat.
diff --git a/core/VerdiHints.v b/core/VerdiHints.v
index 1c8f468c..33e1cde3 100644
--- a/core/VerdiHints.v
+++ b/core/VerdiHints.v
@@ -1,6 +1,4 @@
-Require Import StructTact.Util.
+From StructTact Require Import Util.
 
-#[global]
-Hint Resolve app_cons_in : core.
-#[global]
-Hint Resolve app_cons_in_rest : core.
+#[global] Hint Resolve app_cons_in : core.
+#[global] Hint Resolve app_cons_in_rest : core.
diff --git a/extraction/ExtrOcamlBasicExt.v b/extraction/ExtrOcamlBasicExt.v
index 9c25d03c..60ac1c8a 100644
--- a/extraction/ExtrOcamlBasicExt.v
+++ b/extraction/ExtrOcamlBasicExt.v
@@ -1,4 +1,4 @@
-Require Extraction.
+From Coq Require Extraction.
 
 Extract Inlined Constant fst => "fst".
 Extract Inlined Constant snd => "snd".
diff --git a/extraction/ExtrOcamlBool.v b/extraction/ExtrOcamlBool.v
index 5272d32d..9021dbb6 100644
--- a/extraction/ExtrOcamlBool.v
+++ b/extraction/ExtrOcamlBool.v
@@ -1,5 +1,5 @@
-Require Import Bool.
-Require Extraction.
+From Coq Require Import Bool.
+From Coq Require Extraction.
 
 Extract Inlined Constant negb => "not".
 
diff --git a/extraction/ExtrOcamlDiskOp.v b/extraction/ExtrOcamlDiskOp.v
index 3c5b31ec..42d9e09f 100644
--- a/extraction/ExtrOcamlDiskOp.v
+++ b/extraction/ExtrOcamlDiskOp.v
@@ -1,4 +1,4 @@
-Require Import Verdi.Net.
-Require Extraction.
+From Verdi Require Import Net.
+From Coq Require Extraction.
 
 Extract Inductive disk_op => "DiskOpShim.disk_op" ["DiskOpShim.Append" "DiskOpShim.Write" "DiskOpShim.Delete"].
diff --git a/extraction/ExtrOcamlFinInt.v b/extraction/ExtrOcamlFinInt.v
index 58462932..0a256ca4 100644
--- a/extraction/ExtrOcamlFinInt.v
+++ b/extraction/ExtrOcamlFinInt.v
@@ -1,5 +1,5 @@
-Require Import StructTact.Fin.
-Require Extraction.
+From StructTact Require Import Fin.
+From Coq Require Extraction.
 
 Extract Inlined Constant fin => int.
 
diff --git a/extraction/ExtrOcamlList.v b/extraction/ExtrOcamlList.v
index 374c4e19..bb9df4bd 100644
--- a/extraction/ExtrOcamlList.v
+++ b/extraction/ExtrOcamlList.v
@@ -1,5 +1,5 @@
-Require Import List.
-Require Extraction.
+From Coq Require Import List.
+From Coq Require Extraction.
 
 Extract Inlined Constant length => "List.length".
 Extract Inlined Constant app => "List.append".
diff --git a/extraction/ExtrOcamlNatIntExt.v b/extraction/ExtrOcamlNatIntExt.v
index 6efb72a4..570a5993 100644
--- a/extraction/ExtrOcamlNatIntExt.v
+++ b/extraction/ExtrOcamlNatIntExt.v
@@ -1,6 +1,5 @@
-Require Import PeanoNat.
-Require Import Ascii.
-Require Extraction.
+From Coq Require Import PeanoNat Ascii.
+From Coq Require Extraction.
 
 Extract Inlined Constant Nat.max => "Pervasives.max".
 Extract Inlined Constant Nat.min => "Pervasives.min".
diff --git a/lib/FMapVeryWeak.v b/lib/FMapVeryWeak.v
index 8999f0b5..9a12d52c 100644
--- a/lib/FMapVeryWeak.v
+++ b/lib/FMapVeryWeak.v
@@ -1,16 +1,8 @@
-Require Import ZArith.
-
-Require Import FMapInterface.
-Require Import FMapPositive.
-Require Import FMapList.
-Require Import FMapFacts.
-
-Require Import String.
-Require Import Ascii.
-Require Import List.
-
-Require Import StructTact.StructTactics.
-Require Import StructTact.StringOrders.
+From Coq Require Import ZArith.
+From Coq Require Import FMapInterface FMapPositive.
+From Coq Require Import FMapList FMapFacts.
+From Coq Require Import String Ascii List.
+From StructTact Require Import StructTactics StringOrders.
 
 Import ListNotations.
 
@@ -20,8 +12,8 @@ Module Type VWS.
   Declare Module E : DecidableType.
 
   Definition key := E.t.
-#[global]
-  Hint Transparent key : core.
+
+  #[global] Hint Transparent key : core.
 
   Parameter t : Type -> Type.
 
diff --git a/lib/Ssrexport.v b/lib/Ssrexport.v
index c3d6638b..9928347c 100644
--- a/lib/Ssrexport.v
+++ b/lib/Ssrexport.v
@@ -1,4 +1,4 @@
 From Coq Require Export ssreflect.
-Global Set SsrOldRewriteGoalsOrder.
-Global Set Asymmetric Patterns.
-Global Set Bullet Behavior "None".
+#[export] Set SsrOldRewriteGoalsOrder.
+#[export] Set Asymmetric Patterns.
+#[export] Set Bullet Behavior "None".
diff --git a/systems/Counter.v b/systems/Counter.v
index d9b3d2d8..05ae2609 100644
--- a/systems/Counter.v
+++ b/systems/Counter.v
@@ -1,5 +1,4 @@
-Require Import Verdi.Verdi.
-Require Import Verdi.HandlerMonad.
+From Verdi Require Import Verdi HandlerMonad.
 
 Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
diff --git a/systems/LockServ.v b/systems/LockServ.v
index db84b053..ded59478 100644
--- a/systems/LockServ.v
+++ b/systems/LockServ.v
@@ -1,11 +1,9 @@
-Require Import Verdi.Verdi.
-Require Import Verdi.HandlerMonad.
-Require Import StructTact.Fin.
+From Verdi Require Import Verdi HandlerMonad.
+From StructTact Require Import Fin.
+From Verdi Require Import StatePacketPacketDecomposition.
 
 Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
-Require Import Verdi.StatePacketPacketDecomposition.
-
 Set Implicit Arguments.
 
 Section LockServ.
diff --git a/systems/LockServSeqNum.v b/systems/LockServSeqNum.v
index f8681510..b3daab33 100644
--- a/systems/LockServSeqNum.v
+++ b/systems/LockServSeqNum.v
@@ -1,8 +1,6 @@
-Require Import Verdi.Verdi.
-
-Require Import Verdi.LockServ.
-Require Verdi.SeqNum.
-Require Import Verdi.SeqNumCorrect.
+From Verdi Require Import Verdi LockServ.
+From Verdi Require SeqNum.
+From Verdi Require Import SeqNumCorrect.
 
 Section LockServSeqNum.
 
diff --git a/systems/Log.v b/systems/Log.v
index 848945c5..10fab448 100644
--- a/systems/Log.v
+++ b/systems/Log.v
@@ -1,6 +1,5 @@
-Require Import Verdi.Verdi.
-
-Require Import Cheerios.Cheerios.
+From Verdi Require Import Verdi.
+From Cheerios Require Import Cheerios.
 
 Import DeserializerNotations.
 
diff --git a/systems/LogCorrect.v b/systems/LogCorrect.v
index 68833a8a..e28e1b3d 100644
--- a/systems/LogCorrect.v
+++ b/systems/LogCorrect.v
@@ -1,8 +1,7 @@
-Require Import Verdi.Verdi.
-Require Import Cheerios.Cheerios.
-
-Require Import Verdi.Log.
-Require Import FunctionalExtensionality.
+From Verdi Require Import Verdi.
+From Cheerios Require Import Cheerios.
+From Verdi Require Import Log.
+From Coq Require Import FunctionalExtensionality.
 
 Section LogCorrect.
   Context {orig_base_params : BaseParams}.
diff --git a/systems/SeqNum.v b/systems/SeqNum.v
index a206c3b5..2d106e11 100644
--- a/systems/SeqNum.v
+++ b/systems/SeqNum.v
@@ -1,4 +1,4 @@
-Require Import Verdi.Verdi.
+From Verdi Require Import Verdi.
 
 Set Implicit Arguments.
 
diff --git a/systems/SerializedMsgParams.v b/systems/SerializedMsgParams.v
index 76a9ff7c..549e83ce 100644
--- a/systems/SerializedMsgParams.v
+++ b/systems/SerializedMsgParams.v
@@ -1,5 +1,6 @@
-Require Import Verdi.Verdi.
-Require Import Cheerios.Cheerios.
+From Verdi Require Import Verdi.
+From Cheerios Require Import Cheerios.
+
 Set Implicit Arguments.
 
 Section Serialized.
diff --git a/systems/SerializedMsgParamsCorrect.v b/systems/SerializedMsgParamsCorrect.v
index bf58585c..1f8192d1 100644
--- a/systems/SerializedMsgParamsCorrect.v
+++ b/systems/SerializedMsgParamsCorrect.v
@@ -1,15 +1,10 @@
-Require Import StructTact.Util.
-Require Import Verdi.Verdi.
-
-Require Import FunctionalExtensionality.
-
-Require Import Verdi.TotalMapSimulations.
-Require Import Verdi.PartialMapSimulations.
-
-Require Import Cheerios.Cheerios.
-Require Import Verdi.SerializedMsgParams.
-
-Require Import Verdi.Ssrexport.
+From StructTact Require Import Util.
+From Verdi Require Import Verdi.
+From Coq Require Import FunctionalExtensionality.
+From Verdi Require Import TotalMapSimulations PartialMapSimulations.
+From Cheerios Require Import Cheerios.
+From Verdi Require Import SerializedMsgParams.
+From Verdi Require Import Ssrexport.
 
 Section SerializedMsgCorrect.
   Context {orig_base_params : BaseParams}.
diff --git a/systems/VarD.v b/systems/VarD.v
index f1c68ac5..c2981ab9 100644
--- a/systems/VarD.v
+++ b/systems/VarD.v
@@ -1,10 +1,6 @@
-Require Import Verdi.Verdi.
-
-Require Import FMapList.
-Require Import String.
-
-Require Import Verdi.FMapVeryWeak.
-Require Import Verdi.StateMachineHandlerMonad.
+From Verdi Require Import Verdi.
+From Coq Require Import FMapList String.
+From Verdi Require Import FMapVeryWeak StateMachineHandlerMonad.
 
 Definition key := string.
 Definition value := string.
diff --git a/systems/VarDPrimaryBackup.v b/systems/VarDPrimaryBackup.v
index 7b6a3f23..ebf51c85 100644
--- a/systems/VarDPrimaryBackup.v
+++ b/systems/VarDPrimaryBackup.v
@@ -1,9 +1,6 @@
-Require Import Verdi.Verdi.
-
-Require Import String.
-
-Require Import Verdi.VarD.
-Require Import Verdi.PrimaryBackup.
+From Verdi Require Import Verdi.
+From Coq Require Import String.
+From Verdi Require Import VarD PrimaryBackup.
 
 Open Scope string_scope.