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.