consistently use From-Require

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.

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.
 

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.
 

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.

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) :=
   {

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.
 

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.

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.
 

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

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

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) := 

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.
 

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

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}.

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

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) :=

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) :=
   {

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.

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.

extraction/ExtrOcamlBasicExt.v

@@ -1,4 +1,4 @@
-Require Extraction.
+From Coq Require Extraction.
 
 Extract Inlined Constant fst => "fst".
 Extract Inlined Constant snd => "snd".

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".
 

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"].

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.
 

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".

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".

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.
 

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".