diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 1531deb78..c18827e82 100644 --- a/.github/workflows/coq.yml +++ b/.github/workflows/coq.yml @@ -11,7 +11,7 @@ jobs: strategy: fail-fast: false matrix: - coq-version: [ "dev" , "9.0" , "8.20" , "8.19" ] + coq-version: [ "dev" , "9.1" , "9.0" ] targets: [ "fiat-core parsers parsers-examples coq-ci" ] name: ${{ matrix.coq-version }} (${{ matrix.targets }}) diff --git a/Bedrock/Nomega.v b/Bedrock/Nomega.v index e550d0062..b2de21181 100644 --- a/Bedrock/Nomega.v +++ b/Bedrock/Nomega.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (* Make [omega] work for [N] *) -Require Import Coq.Arith.Arith Coq.ZArith.ZArith Coq.NArith.NArith. +Require Import Stdlib.Arith.Arith Stdlib.ZArith.ZArith Stdlib.NArith.NArith. Local Open Scope N_scope. diff --git a/Bedrock/Word.v b/Bedrock/Word.v index 0e8b8ab88..a4b3484bb 100644 --- a/Bedrock/Word.v +++ b/Bedrock/Word.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** Fixed precision machine words *) -Require Import Coq.Arith.Arith +Require Import Stdlib.Arith.Arith Coq.NArith.NArith Coq.Bool.Bool Coq.ZArith.ZArith. @@ -283,7 +283,7 @@ Qed. Hint Resolve shatter_word_0. -Require Import Coq.Logic.Eqdep_dec. +Require Import Stdlib.Logic.Eqdep_dec. Definition weq : forall sz (x y : word sz), {x = y} + {x <> y}. refine (fix weq sz (x : word sz) : forall y : word sz, {x = y} + {x <> y} := @@ -369,7 +369,7 @@ Theorem split2_combine : forall sz1 sz2 (w : word sz1) (z : word sz2), induction sz1; shatterer. Qed. -Require Import Coq.Logic.Eqdep_dec. +Require Import Stdlib.Logic.Eqdep_dec. Theorem combine_assoc : forall n1 (w1 : word n1) n2 n3 (w2 : word n2) (w3 : word n3) Heq, diff --git a/src/ADT/ADTHide.v b/src/ADT/ADTHide.v index 1892359be..ffadc6b6c 100644 --- a/src/ADT/ADTHide.v +++ b/src/ADT/ADTHide.v @@ -1,4 +1,5 @@ -Require Import Fiat.Common Fiat.Computation.Core Fiat.ADT.Core Coq.Sets.Ensembles. +Require Import Fiat.Common Fiat.Computation.Core Fiat.ADT.Core. +From Stdlib Require Import Ensembles. Section HideADT. diff --git a/src/ADT/ComputationalADT.v b/src/ADT/ComputationalADT.v index 222dcb0fa..38826ec1d 100644 --- a/src/ADT/ComputationalADT.v +++ b/src/ADT/ComputationalADT.v @@ -1,5 +1,5 @@ Require Export Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT. -Require Import Coq.Sets.Ensembles. +From Stdlib Require Import Ensembles. Generalizable All Variables. Set Implicit Arguments. diff --git a/src/ADT/Core.v b/src/ADT/Core.v index 1831f1255..ece1e03c5 100644 --- a/src/ADT/Core.v +++ b/src/ADT/Core.v @@ -1,5 +1,5 @@ Require Export Fiat.Common Fiat.Computation Fiat.ADT.ADTSig. -Require Import Coq.Sets.Ensembles. +From Stdlib Require Import Ensembles. Generalizable All Variables. Set Implicit Arguments. diff --git a/src/ADTInduction.v b/src/ADTInduction.v index 6c4c78096..d2f29bc97 100644 --- a/src/ADTInduction.v +++ b/src/ADTInduction.v @@ -1,7 +1,7 @@ Require Import Fiat.ADT Fiat.ADTNotation. -Require Import Coq.Sets.Ensembles. -Require Import Coq.Lists.List. +From Stdlib Require Import Ensembles. +From Stdlib Require Import List. Import ListNotations. diff --git a/src/ADTNotation/BuildADT.v b/src/ADTNotation/BuildADT.v index 56709799c..a0a36e472 100644 --- a/src/ADTNotation/BuildADT.v +++ b/src/ADTNotation/BuildADT.v @@ -1,7 +1,5 @@ -Require Import Coq.Sets.Ensembles - Coq.Lists.List - Coq.Strings.String - Fiat.Common +From Stdlib Require Import Ensembles List String. +Require Import Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core diff --git a/src/ADTNotation/BuildADTReplaceMethods.v b/src/ADTNotation/BuildADTReplaceMethods.v index df1dc6bc2..c0fef2f23 100644 --- a/src/ADTNotation/BuildADTReplaceMethods.v +++ b/src/ADTNotation/BuildADTReplaceMethods.v @@ -1,6 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String - Fiat.ADT.ADTSig +From Stdlib Require Import List String. +Require Import Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.Common Fiat.Common.BoundedLookup diff --git a/src/ADTNotation/BuildADTSig.v b/src/ADTNotation/BuildADTSig.v index 0f624c66b..d4b5d9736 100644 --- a/src/ADTNotation/BuildADTSig.v +++ b/src/ADTNotation/BuildADTSig.v @@ -1,5 +1,5 @@ Require Import Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.ADT.ADTSig. -Require Import Coq.Lists.List Coq.Strings.String. +From Stdlib Require Import List String. (* Notation for ADT Signatures. *) @@ -102,7 +102,7 @@ Delimit Scope ADTSig_scope with ADTSig. (* Notation for ADT signatures utilizing [BuildADTSig]. *) -Require Import Coq.Vectors.Vector. +From Stdlib Require Import Vector. Import Vectors.Vector.VectorNotations. Delimit Scope vector_scope with vector. diff --git a/src/ADTNotation/BuildComputationalADT.v b/src/ADTNotation/BuildComputationalADT.v index 402f6ebbf..3325d6d4f 100644 --- a/src/ADTNotation/BuildComputationalADT.v +++ b/src/ADTNotation/BuildComputationalADT.v @@ -1,8 +1,5 @@ -Require Import - Coq.Sets.Ensembles - Coq.Lists.List - Coq.Strings.String - Fiat.Common +From Stdlib Require Import Ensembles List String. +Require Import Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core diff --git a/src/ADTRefinement/BuildADTRefinements/AddCache.v b/src/ADTRefinement/BuildADTRefinements/AddCache.v index e873b66c7..19073ae6a 100644 --- a/src/ADTRefinement/BuildADTRefinements/AddCache.v +++ b/src/ADTRefinement/BuildADTRefinements/AddCache.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Fiat.Common +Require Import Stdlib.Lists.List Fiat.Common Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT Fiat.Common.ilist Fiat.Common.BoundedLookup diff --git a/src/ADTRefinement/BuildADTRefinements/HoneRepresentation.v b/src/ADTRefinement/BuildADTRefinements/HoneRepresentation.v index f6d705ef7..ee18150ca 100644 --- a/src/ADTRefinement/BuildADTRefinements/HoneRepresentation.v +++ b/src/ADTRefinement/BuildADTRefinements/HoneRepresentation.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Fiat.Common +Require Import Stdlib.Lists.List Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.IterateBoundedIndex diff --git a/src/ADTRefinement/BuildADTRefinements/RefineAllMethods.v b/src/ADTRefinement/BuildADTRefinements/RefineAllMethods.v index 745f9a014..902b8402e 100644 --- a/src/ADTRefinement/BuildADTRefinements/RefineAllMethods.v +++ b/src/ADTRefinement/BuildADTRefinements/RefineAllMethods.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Fiat.Common +Require Import Stdlib.Lists.List Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.IterateBoundedIndex diff --git a/src/ADTRefinement/BuildADTRefinements/SimplifyRep.v b/src/ADTRefinement/BuildADTRefinements/SimplifyRep.v index c63602f25..26b2fcec7 100644 --- a/src/ADTRefinement/BuildADTRefinements/SimplifyRep.v +++ b/src/ADTRefinement/BuildADTRefinements/SimplifyRep.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Fiat.Common +Require Import Stdlib.Lists.List Fiat.Common Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT Fiat.Common.ilist Fiat.Common.BoundedLookup diff --git a/src/ADTRefinement/Core.v b/src/ADTRefinement/Core.v index 16e3750fe..bc9eddd10 100644 --- a/src/ADTRefinement/Core.v +++ b/src/ADTRefinement/Core.v @@ -1,4 +1,5 @@ -Require Import Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles. +Require Import Fiat.Common Fiat.Computation Fiat.ADT. +From Stdlib Require Import Ensembles. Generalizable All Variables. Set Implicit Arguments. diff --git a/src/ADTRefinement/FixedPoint.v b/src/ADTRefinement/FixedPoint.v index b7a4a9379..1b0e846ea 100644 --- a/src/ADTRefinement/FixedPoint.v +++ b/src/ADTRefinement/FixedPoint.v @@ -1,8 +1,8 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import Fiat.ADT Fiat.ADTNotation. Require Export Fiat.Computation.FixComp. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Arith.PeanoNat. +From Stdlib Require Import ZArith. +Require Import Stdlib.Arith.PeanoNat. Import LeastFixedPointFun. diff --git a/src/ADTRefinement/GeneralBuildADTRefinements.v b/src/ADTRefinement/GeneralBuildADTRefinements.v index ffd74a6ef..bf6387aa9 100644 --- a/src/ADTRefinement/GeneralBuildADTRefinements.v +++ b/src/ADTRefinement/GeneralBuildADTRefinements.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List Coq.Arith.Arith - Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core +From Stdlib Require Import List Arith. +Require Import Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADT.ComputationalADT Fiat.Common.BoundedLookup Fiat.Common.ilist @@ -16,7 +16,7 @@ Require Import Coq.Lists.List Coq.Arith.Arith Section BuildADTRefinements. - Require Import Coq.Strings.String. + From Stdlib Require Import String. Local Hint Resolve string_dec. Lemma refineADT_BuildADT_ReplaceConstructor diff --git a/src/ADTRefinement/GeneralBuildADTTactics.v b/src/ADTRefinement/GeneralBuildADTTactics.v index e155f9fad..8fd4c1efe 100644 --- a/src/ADTRefinement/GeneralBuildADTTactics.v +++ b/src/ADTRefinement/GeneralBuildADTTactics.v @@ -1,6 +1,6 @@ Require Export Fiat.ADTRefinement.GeneralBuildADTRefinements. (* TODO: Clean out these imports. *) -Require Import Coq.Lists.List Coq.Arith.Arith +Require Import Stdlib.Lists.List Stdlib.Arith.Arith Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADT.ComputationalADT Fiat.Common.BoundedLookup diff --git a/src/ADTRefinement/GeneralRefinements.v b/src/ADTRefinement/GeneralRefinements.v index 2da9ddd4e..097ed28ff 100644 --- a/src/ADTRefinement/GeneralRefinements.v +++ b/src/ADTRefinement/GeneralRefinements.v @@ -1,6 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String - Fiat.Common +From Stdlib Require Import List String. +Require Import Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.ADT.Core diff --git a/src/ADTRefinement/Refinements/ADTCache.v b/src/ADTRefinement/Refinements/ADTCache.v index 49ebe4384..1c64b6cf3 100644 --- a/src/ADTRefinement/Refinements/ADTCache.v +++ b/src/ADTRefinement/Refinements/ADTCache.v @@ -1,4 +1,4 @@ -Require Import Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv. +Require Import Fiat.Common Fiat.Computation Fiat.ADT Stdlib.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv. Generalizable All Variables. Set Implicit Arguments. diff --git a/src/ADTRefinement/Refinements/ADTRepInv.v b/src/ADTRefinement/Refinements/ADTRepInv.v index 0f0adf9fb..7b520e23e 100644 --- a/src/ADTRefinement/Refinements/ADTRepInv.v +++ b/src/ADTRefinement/Refinements/ADTRepInv.v @@ -1,4 +1,4 @@ -Require Import Fiat.Common Fiat.Computation Coq.Sets.Ensembles +Require Import Fiat.Common Fiat.Computation Stdlib.Sets.Ensembles Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.GeneralRefinements. diff --git a/src/ADTRefinement/SetoidMorphisms.v b/src/ADTRefinement/SetoidMorphisms.v index 32dfa420f..e7f46f6d8 100644 --- a/src/ADTRefinement/SetoidMorphisms.v +++ b/src/ADTRefinement/SetoidMorphisms.v @@ -1,4 +1,5 @@ -Require Import Fiat.Common Fiat.Computation Coq.Sets.Ensembles. +Require Import Fiat.Common Fiat.Computation. +From Stdlib Require Import Ensembles. Require Import Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core. (** Definitions for integrating [refineADT] into the setoid rewriting diff --git a/src/CertifiedExtraction/Benchmarks/DNS.v b/src/CertifiedExtraction/Benchmarks/DNS.v index ed7981a8e..0830f793d 100644 --- a/src/CertifiedExtraction/Benchmarks/DNS.v +++ b/src/CertifiedExtraction/Benchmarks/DNS.v @@ -6,7 +6,7 @@ Require Import Opaque Transformer.transform_id. Opaque EncodeAndPad. (* FIXME move *) -Require Import Coq.Program.Program. +From Stdlib Require Import Program. Definition PacketAsCollectionOfVariables {av} vid vmask vquestion vanswer vauthority vadditional (p: packet_t) diff --git a/src/CertifiedExtraction/Benchmarks/MicroEncodersSetup.v b/src/CertifiedExtraction/Benchmarks/MicroEncodersSetup.v index 4b3b25d2d..8b0dc2258 100644 --- a/src/CertifiedExtraction/Benchmarks/MicroEncodersSetup.v +++ b/src/CertifiedExtraction/Benchmarks/MicroEncodersSetup.v @@ -12,7 +12,7 @@ Require Export Fiat.CertifiedExtraction.Extraction.BinEncoders.BinEncoders. Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector. Require Export diff --git a/src/CertifiedExtraction/Benchmarks/results/ProcessSchedulerExtractedMethods.v b/src/CertifiedExtraction/Benchmarks/results/ProcessSchedulerExtractedMethods.v index 51464550b..e4462bd5e 100644 --- a/src/CertifiedExtraction/Benchmarks/results/ProcessSchedulerExtractedMethods.v +++ b/src/CertifiedExtraction/Benchmarks/results/ProcessSchedulerExtractedMethods.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String. +From Stdlib Require Import String. Require Import Bedrock.Platform.Facade.DFacade. Require Import Bedrock.Platform.Cito.SyntaxExpr. diff --git a/src/CertifiedExtraction/Core.v b/src/CertifiedExtraction/Core.v index 6939295e7..800d49d93 100644 --- a/src/CertifiedExtraction/Core.v +++ b/src/CertifiedExtraction/Core.v @@ -1,4 +1,4 @@ -Require Export Coq.Strings.String. +Require Export Stdlib.Strings.String. Require Export Computation.Core ADTRefinement. Require Export Bedrock.Platform.Facade.DFacade Bedrock.Platform.Cito.StringMap. diff --git a/src/CertifiedExtraction/CoreLemmas.v b/src/CertifiedExtraction/CoreLemmas.v index f3a7915d1..1c8f2e776 100644 --- a/src/CertifiedExtraction/CoreLemmas.v +++ b/src/CertifiedExtraction/CoreLemmas.v @@ -4,7 +4,7 @@ Require Export CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils. -Require Export Coq.Setoids.Setoid. +Require Export Stdlib.Setoids.Setoid. Local Open Scope map_scope. Local Open Scope telescope_scope. diff --git a/src/CertifiedExtraction/Extraction/BinEncoders/Basics.v b/src/CertifiedExtraction/Extraction/BinEncoders/Basics.v index b52214b20..d594f3350 100644 --- a/src/CertifiedExtraction/Extraction/BinEncoders/Basics.v +++ b/src/CertifiedExtraction/Extraction/BinEncoders/Basics.v @@ -1,4 +1,4 @@ -Require Export Coq.NArith.NArith. +Require Export Stdlib.NArith.NArith. Require Export Bedrock.Memory Bedrock.Word. Require Export diff --git a/src/CertifiedExtraction/Extraction/BinEncoders/BinEncoders.v b/src/CertifiedExtraction/Extraction/BinEncoders/BinEncoders.v index b3c89e3e9..5e7e6987c 100644 --- a/src/CertifiedExtraction/Extraction/BinEncoders/BinEncoders.v +++ b/src/CertifiedExtraction/Extraction/BinEncoders/BinEncoders.v @@ -7,7 +7,7 @@ Require Export Fiat.CertifiedExtraction.Extraction.BinEncoders.RewriteRules. Unset Implicit Arguments. -Require Import Coq.Lists.List. +From Stdlib Require Import List. Ltac _compile_decide_padding_0 := repeat first [ reflexivity | diff --git a/src/CertifiedExtraction/Extraction/BinEncoders/Properties.v b/src/CertifiedExtraction/Extraction/BinEncoders/Properties.v index 5a6d00c73..0d96e13f9 100644 --- a/src/CertifiedExtraction/Extraction/BinEncoders/Properties.v +++ b/src/CertifiedExtraction/Extraction/BinEncoders/Properties.v @@ -23,7 +23,7 @@ Proof. destruct (encode1 _); simpl; destruct (encode2 _); reflexivity. Qed. -Require Import Coq.Lists.List. +From Stdlib Require Import List. Require Import Bedrock.Word. Theorem exist_irrel : forall A (P : A -> Prop) x1 pf1 x2 pf2, diff --git a/src/CertifiedExtraction/Extraction/BinEncoders/Wrappers.v b/src/CertifiedExtraction/Extraction/BinEncoders/Wrappers.v index c63dae0c5..9b1e4ecc2 100644 --- a/src/CertifiedExtraction/Extraction/BinEncoders/Wrappers.v +++ b/src/CertifiedExtraction/Extraction/BinEncoders/Wrappers.v @@ -1,4 +1,4 @@ -Require Import Coq.Program.Program. +From Stdlib Require Import Program. Require Import Fiat.CertifiedExtraction.Core diff --git a/src/CertifiedExtraction/Extraction/Core.v b/src/CertifiedExtraction/Extraction/Core.v index 437160fcb..6f8378ece 100644 --- a/src/CertifiedExtraction/Extraction/Core.v +++ b/src/CertifiedExtraction/Extraction/Core.v @@ -10,7 +10,7 @@ Require Export CertifiedExtraction.Extraction.Gensym CertifiedExtraction.Extraction.PreconditionSets. -Require Import Coq.Strings.String. +From Stdlib Require Import String. Global Open Scope string_scope. Ltac av_from_ext ext := diff --git a/src/CertifiedExtraction/Extraction/External/ScalarMethods.v b/src/CertifiedExtraction/Extraction/External/ScalarMethods.v index 3c927a7e3..3db25fc3f 100644 --- a/src/CertifiedExtraction/Extraction/External/ScalarMethods.v +++ b/src/CertifiedExtraction/Extraction/External/ScalarMethods.v @@ -2,7 +2,7 @@ Require Import CertifiedExtraction.Extraction.External.Core CertifiedExtraction.Extraction.External.GenericMethods. -Require Import Coq.Lists.List. +From Stdlib Require Import List. Lemma CompileCallFacadeImplementationWW: forall {av} {env} fWW, diff --git a/src/CertifiedExtraction/Extraction/Extraction.v b/src/CertifiedExtraction/Extraction/Extraction.v index 50431f40e..5f94dbffe 100644 --- a/src/CertifiedExtraction/Extraction/Extraction.v +++ b/src/CertifiedExtraction/Extraction/Extraction.v @@ -1,5 +1,5 @@ Require Export - Coq.Strings.String + Stdlib.Strings.String CertifiedExtraction.FacadeNotations CertifiedExtraction.Extraction.External.External. Require Import diff --git a/src/CertifiedExtraction/Extraction/Gensym.v b/src/CertifiedExtraction/Extraction/Gensym.v index e250e7f77..30bb1d4bb 100644 --- a/src/CertifiedExtraction/Extraction/Gensym.v +++ b/src/CertifiedExtraction/Extraction/Gensym.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Numbers.Natural.Peano.NPeano - Coq.Strings.String +Require Import Stdlib.Numbers.Natural.Peano.NPeano + Stdlib.Strings.String Coq.Arith.Lt Coq.Arith.Compare_dec Coq.Lists.List diff --git a/src/CertifiedExtraction/Extraction/QueryStructures/CallRules/Core.v b/src/CertifiedExtraction/Extraction/QueryStructures/CallRules/Core.v index 229c16014..ba755f744 100644 --- a/src/CertifiedExtraction/Extraction/QueryStructures/CallRules/Core.v +++ b/src/CertifiedExtraction/Extraction/QueryStructures/CallRules/Core.v @@ -1,4 +1,4 @@ -Require Export Coq.Program.Program. +Require Export Stdlib.Program.Program. Require Export CertifiedExtraction.Extraction.QueryStructures.Basics. Require Export CertifiedExtraction.Extraction.QueryStructures.TupleToListW. Require Export CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW. diff --git a/src/CertifiedExtraction/Extraction/QueryStructures/EnsemblesOfTuplesAndListW.v b/src/CertifiedExtraction/Extraction/QueryStructures/EnsemblesOfTuplesAndListW.v index 8cfd5f504..ada6e7468 100644 --- a/src/CertifiedExtraction/Extraction/QueryStructures/EnsemblesOfTuplesAndListW.v +++ b/src/CertifiedExtraction/Extraction/QueryStructures/EnsemblesOfTuplesAndListW.v @@ -176,7 +176,7 @@ Hint Rewrite @EnsembleIndexedListEquivalence_TupleToListW_UnIndexedEquiv_Characterisation : EnsembleIndexedListEquivalence_TupleToListW_UnIndexedEquiv. -Require Import Coq.Strings.String. +From Stdlib Require Import String. Lemma EnsembleIndexedListEquivalence_TupleToListW_UnIndexedEquiv: forall (n : nat) (lst : list (FiatWTuple n)) (ens : FiatWBag n), diff --git a/src/CertifiedExtraction/FMapUtils.v b/src/CertifiedExtraction/FMapUtils.v index cefccabed..783603427 100644 --- a/src/CertifiedExtraction/FMapUtils.v +++ b/src/CertifiedExtraction/FMapUtils.v @@ -1,4 +1,4 @@ -Require Import Coq.FSets.FMaps. +Require Import Stdlib.FSets.FMaps. Require Import CertifiedExtraction.PureUtils. Module WMoreFacts_fun (E:DecidableType) (Import M:WSfun E). diff --git a/src/CertifiedExtraction/FacadeLemmas.v b/src/CertifiedExtraction/FacadeLemmas.v index ccacaa92e..46955d944 100644 --- a/src/CertifiedExtraction/FacadeLemmas.v +++ b/src/CertifiedExtraction/FacadeLemmas.v @@ -3,7 +3,7 @@ Require Import CertifiedExtraction.PureUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.FacadeUtils. -Require Import Coq.Setoids.Setoid. +From Stdlib Require Import Setoid. Lemma NotIn_not_mapsto_adt : forall {av} var (state: StringMap.t (Value av)), diff --git a/src/CertifiedExtraction/FacadeNotations.v b/src/CertifiedExtraction/FacadeNotations.v index 6d1b09103..48678c289 100644 --- a/src/CertifiedExtraction/FacadeNotations.v +++ b/src/CertifiedExtraction/FacadeNotations.v @@ -4,7 +4,7 @@ Require Import Bedrock.Platform.Cito.StringMap Bedrock.Platform.Cito.SyntaxExpr Bedrock.Memory. -Require Import Coq.Strings.String. +From Stdlib Require Import String. Notation "A ; B" := (Seq A B) (at level 201, B at level 201, diff --git a/src/CertifiedExtraction/FacadeUtils.v b/src/CertifiedExtraction/FacadeUtils.v index f17103596..8de6e8688 100644 --- a/src/CertifiedExtraction/FacadeUtils.v +++ b/src/CertifiedExtraction/FacadeUtils.v @@ -12,7 +12,7 @@ Require Import CertifiedExtraction.StringMapUtils CertifiedExtraction.PureFacadeLemmas. Require Import - Coq.Strings.String. + Stdlib.Strings.String. Require Export CertifiedExtraction.FacadeWrappers. diff --git a/src/CertifiedExtraction/PropertiesOfTelescopes.v b/src/CertifiedExtraction/PropertiesOfTelescopes.v index 1b44fa2a5..f4404c52a 100644 --- a/src/CertifiedExtraction/PropertiesOfTelescopes.v +++ b/src/CertifiedExtraction/PropertiesOfTelescopes.v @@ -18,7 +18,7 @@ Ltac TelEq_rel_t := | _ => solve [intuition] end. -Require Import Coq.Setoids.Setoid. +From Stdlib Require Import Setoid. Lemma TelEq_refl {A ext}: Reflexive (@TelEq A ext). diff --git a/src/CertifiedExtraction/PureFacadeLemmas.v b/src/CertifiedExtraction/PureFacadeLemmas.v index ec067603d..6c14b40eb 100644 --- a/src/CertifiedExtraction/PureFacadeLemmas.v +++ b/src/CertifiedExtraction/PureFacadeLemmas.v @@ -1,7 +1,7 @@ Require Export Bedrock.Platform.Cito.StringMap Bedrock.Platform.Cito.StringMapFacts. Require Export Bedrock.Platform.Cito.SyntaxExpr Bedrock.Platform.Facade.DFacade. Require Import Bedrock.Platform.Facade.DFacadeFacts2. -Require Import Coq.Setoids.Setoid. +From Stdlib Require Import Setoid. Add Parametric Morphism {av} : (@eval av) with signature (StringMap.Equal ==> eq ==> eq) diff --git a/src/CertifiedExtraction/RemoveSkips.v b/src/CertifiedExtraction/RemoveSkips.v index 3c20a0b38..7c878284f 100644 --- a/src/CertifiedExtraction/RemoveSkips.v +++ b/src/CertifiedExtraction/RemoveSkips.v @@ -5,7 +5,7 @@ Require Import Fiat.CertifiedExtraction.FacadeUtils Fiat.CertifiedExtraction.FacadeNotations. -Require Import Coq.Program.Program. +From Stdlib Require Import Program. Definition Is_Skip : forall p, { p = Skip } + { p <> Skip }. destruct p; diff --git a/src/CertifiedExtraction/StringMapUtils.v b/src/CertifiedExtraction/StringMapUtils.v index 5ef81a351..8469a5026 100644 --- a/src/CertifiedExtraction/StringMapUtils.v +++ b/src/CertifiedExtraction/StringMapUtils.v @@ -27,7 +27,7 @@ Hint Resolve urgh : typeclass_instances. (* (* Inifinite loop unless `urgh' is added as a hint *) *) (* Abort. *) -Require Import Coq.Setoids.Setoid. +From Stdlib Require Import Setoid. Add Parametric Morphism {av} : (@StringMap.find av) with signature (eq ==> StringMap.Equal ==> eq) diff --git a/src/Common.v b/src/Common.v index 441073064..b8dd3f2d6 100644 --- a/src/Common.v +++ b/src/Common.v @@ -1,7 +1,5 @@ -Require Import Coq.Lists.List. -From Coq Require Import ZArith.ZArith SetoidList. -Require Export Coq.Setoids.Setoid Coq.Classes.RelationClasses - Coq.Program.Program Coq.Classes.Morphisms. +From Stdlib Require Import List ZArith SetoidList. +From Stdlib Require Export Setoid RelationClasses Program Morphisms. Require Export Fiat.Common.Tactics.SplitInContext. Require Export Fiat.Common.Tactics.Combinators. Require Export Fiat.Common.Tactics.FreeIn. diff --git a/src/Common/BoolFacts.v b/src/Common/BoolFacts.v index 36465e438..065a9d234 100644 --- a/src/Common/BoolFacts.v +++ b/src/Common/BoolFacts.v @@ -1,5 +1,5 @@ -Require Import Coq.Strings.String Coq.Strings.Ascii Coq.Arith.Arith Coq.ZArith.BinInt Coq.NArith.BinNat Coq.Bool.Bool. -Require Import Coq.Classes.Morphisms. +From Stdlib Require Import String Ascii Arith BinInt BinNat Bool. +From Stdlib Require Import Morphisms. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Local Coercion is_true : bool >-> Sortclass. diff --git a/src/Common/BoundedLookup.v b/src/Common/BoundedLookup.v index 8a5b86e10..18b610448 100644 --- a/src/Common/BoundedLookup.v +++ b/src/Common/BoundedLookup.v @@ -1,11 +1,7 @@ -Require Import Coq.Lists.List - Coq.Strings.String - Coq.Arith.Arith - Coq.Logic.Eqdep_dec - Fiat.Common.ilist - Fiat.Common.ilist2. - -Require Coq.Vectors.Vector. +From Stdlib Require Import List String Arith Eqdep_dec. +Require Import Fiat.Common.ilist Fiat.Common.ilist2. + +From Stdlib Require Vector. Global Set Asymmetric Patterns. (* Typeclasses for ensuring that a string is included diff --git a/src/Common/DecideableEnsembles.v b/src/Common/DecideableEnsembles.v index 688028f29..e8488d097 100644 --- a/src/Common/DecideableEnsembles.v +++ b/src/Common/DecideableEnsembles.v @@ -1,4 +1,5 @@ -Require Import Fiat.Common Coq.Arith.Arith Coq.Bool.Bool Coq.Sets.Ensembles. +Require Import Fiat.Common. +From Stdlib Require Import Arith Bool Ensembles. Class DecideableEnsemble {A} (P : Ensemble A) := { dec : A -> bool; diff --git a/src/Common/Ensembles/Cardinal.v b/src/Common/Ensembles/Cardinal.v index b91fc6a48..66f88dd89 100644 --- a/src/Common/Ensembles/Cardinal.v +++ b/src/Common/Ensembles/Cardinal.v @@ -1,6 +1,6 @@ (** * Miscellaneous definitions about ensembles *) -Require Import Coq.Lists.List. -Require Export Coq.Sets.Ensembles. +From Stdlib Require Import List. +From Stdlib Require Export Ensembles. Require Import Fiat.Common Fiat.Common.List.PermutationFacts Fiat.Common.Ensembles.EnsembleListEquivalence. (** Coq's [cardinal] is stupid, and not total. For example, it diff --git a/src/Common/Ensembles/EnsembleListEquivalence.v b/src/Common/Ensembles/EnsembleListEquivalence.v index 8cfd90393..e6cad868b 100644 --- a/src/Common/Ensembles/EnsembleListEquivalence.v +++ b/src/Common/Ensembles/EnsembleListEquivalence.v @@ -1,6 +1,6 @@ -Require Import Coq.Lists.List. -Require Export Coq.Sets.Ensembles. -Require Import Coq.Sorting.Permutation. +From Stdlib Require Import List. +From Stdlib Require Export Ensembles. +From Stdlib Require Import Permutation. Require Import Fiat.Common. Require Import Fiat.Common.List.PermutationFacts. diff --git a/src/Common/Ensembles/Equivalence.v b/src/Common/Ensembles/Equivalence.v index 944800729..500df72b4 100644 --- a/src/Common/Ensembles/Equivalence.v +++ b/src/Common/Ensembles/Equivalence.v @@ -1,4 +1,4 @@ -Require Export Coq.Sets.Ensembles. +From Stdlib Require Export Ensembles. Require Import Fiat.Common. Set Implicit Arguments. diff --git a/src/Common/Ensembles/IndexedEnsembles.v b/src/Common/Ensembles/IndexedEnsembles.v index 7dac148c7..200af8322 100644 --- a/src/Common/Ensembles/IndexedEnsembles.v +++ b/src/Common/Ensembles/IndexedEnsembles.v @@ -1,11 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Lists.List - Coq.Strings.String - Coq.ZArith.ZArith - Coq.Logic.FunctionalExtensionality - Coq.Sorting.Permutation Coq.Sets.Ensembles - Fiat.Common.DecideableEnsembles - Fiat.Common.List.PermutationFacts +From Stdlib Require Import List String ZArith FunctionalExtensionality Permutation Ensembles. +Require Import Fiat.Common.DecideableEnsembles Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.Common.List.ListFacts. diff --git a/src/Common/Ensembles/Morphisms.v b/src/Common/Ensembles/Morphisms.v index 4b907f7b1..f97aeedd1 100644 --- a/src/Common/Ensembles/Morphisms.v +++ b/src/Common/Ensembles/Morphisms.v @@ -1,7 +1,7 @@ -Require Export Coq.Sets.Ensembles. +From Stdlib Require Export Ensembles. Require Import Fiat.Common.Ensembles.Equivalence. Require Import Fiat.Common.Ensembles.Tactics. -Require Import Coq.Classes.RelationClasses. +From Stdlib Require Import RelationClasses. Set Implicit Arguments. Require Import Fiat.Common. diff --git a/src/Common/Ensembles/Notations.v b/src/Common/Ensembles/Notations.v index a98ce2988..35ee3af85 100644 --- a/src/Common/Ensembles/Notations.v +++ b/src/Common/Ensembles/Notations.v @@ -1,4 +1,4 @@ -Require Export Coq.Sets.Ensembles. +From Stdlib Require Export Ensembles. Require Export Fiat.Common.ReservedNotations. Delimit Scope Ensemble_scope with ensemble. diff --git a/src/Common/Ensembles/Tactics.v b/src/Common/Ensembles/Tactics.v index 6ddc149e3..499a62616 100644 --- a/src/Common/Ensembles/Tactics.v +++ b/src/Common/Ensembles/Tactics.v @@ -1,4 +1,4 @@ -Require Import Coq.Sets.Ensembles. +From Stdlib Require Import Ensembles. Require Import Fiat.Common. Create HintDb ensembles discriminated. diff --git a/src/Common/EnumType.v b/src/Common/EnumType.v index 4d10efd41..b46f7b444 100644 --- a/src/Common/EnumType.v +++ b/src/Common/EnumType.v @@ -1,6 +1,4 @@ -Require Import - Coq.Vectors.Vector - Coq.Vectors.Vector. +From Stdlib Require Import Vector. Require Import Fiat.Common.BoundedLookup. diff --git a/src/Common/Enumerable.v b/src/Common/Enumerable.v index df38dc10b..a675119d2 100644 --- a/src/Common/Enumerable.v +++ b/src/Common/Enumerable.v @@ -1,6 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import List ZArith. Require Import Fiat.Common.List.Operations. Require Import Fiat.Common.List.ListFacts. Require Import Fiat.Common.StringFacts. diff --git a/src/Common/Enumerable/BoolProp.v b/src/Common/Enumerable/BoolProp.v index 6db801720..0cf1bcd9d 100644 --- a/src/Common/Enumerable/BoolProp.v +++ b/src/Common/Enumerable/BoolProp.v @@ -1,5 +1,5 @@ -Require Import Coq.Arith.Compare_dec. -Require Import Coq.Lists.List. +Require Import Stdlib.Arith.Compare_dec. +From Stdlib Require Import List. Require Import Fiat.Common.UIP. Require Import Fiat.Common.List.Operations. Require Import Fiat.Common.List.ListFacts. diff --git a/src/Common/Equality.v b/src/Common/Equality.v index 75102520d..8fe916152 100644 --- a/src/Common/Equality.v +++ b/src/Common/Equality.v @@ -1,9 +1,5 @@ -From Coq Require Import List SetoidList. -Require Import Coq.Bool.Bool. -Require Import Coq.Arith.PeanoNat. -Require Import Coq.Strings.Ascii. -Require Import Coq.Strings.String. -Require Import Coq.Logic.Eqdep_dec. +From Stdlib Require Import List SetoidList. +From Stdlib Require Import Bool PeanoNat Ascii String Eqdep_dec. Require Import Fiat.Common. Set Implicit Arguments. diff --git a/src/Common/FMapExtensions.v b/src/Common/FMapExtensions.v index 299684ab0..712b61179 100644 --- a/src/Common/FMapExtensions.v +++ b/src/Common/FMapExtensions.v @@ -1,15 +1,14 @@ -Require Export Coq.FSets.FMapInterface. -Require Import Coq.FSets.FMapFacts - Coq.Program.Program - Coq.Structures.OrderedTypeEx - Fiat.Common +From Stdlib Require Export FMapInterface. +From Stdlib Require Import FMapFacts Program OrderedTypeEx. +Require Import Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances. -Require Coq.Sorting.Permutation Fiat.Common.List.PermutationFacts. +From Stdlib Require Permutation. +Require Fiat.Common.List.PermutationFacts. Unset Implicit Arguments. @@ -399,7 +398,7 @@ Module FMapExtensions_fun (E: DecidableType) (Import M: WSfun E). intuition eauto. Qed. - Import Coq.Sorting.Permutation Fiat.Common.List.PermutationFacts. + Import Stdlib.Sorting.Permutation Fiat.Common.List.PermutationFacts. Lemma InA_mapsto_add {Value} : forall bag' kv k' (v' : Value), diff --git a/src/Common/FMapExtensions/Wf.v b/src/Common/FMapExtensions/Wf.v index 16190e4b4..5e4afe04d 100644 --- a/src/Common/FMapExtensions/Wf.v +++ b/src/Common/FMapExtensions/Wf.v @@ -1,4 +1,4 @@ -Require Export Coq.FSets.FMapInterface. +Require Export Stdlib.FSets.FMapInterface. Require Import Fiat.Common.Wf. Require Export Fiat.Common.FMapExtensions. Require Export Fiat.Common.FMapExtensions.LiftRelationInstances. diff --git a/src/Common/FixedPoints.v b/src/Common/FixedPoints.v index 2477f162b..49f460c89 100644 --- a/src/Common/FixedPoints.v +++ b/src/Common/FixedPoints.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Arith.EqNat Coq.Arith.Compare_dec Coq.ZArith.ZArith. -Require Import Coq.Lists.List. +From Stdlib Require Import EqNat Compare_dec ZArith. +From Stdlib Require Import List. Require Import Fiat.Common.List.ListFacts. Require Import Fiat.Common. Set Implicit Arguments. diff --git a/src/Common/Frame.v b/src/Common/Frame.v index f45f34861..317df29d7 100644 --- a/src/Common/Frame.v +++ b/src/Common/Frame.v @@ -1,7 +1,4 @@ -Require Import - SetoidClass - Coq.Classes.Morphisms - Coq.Arith.PeanoNat. +From Stdlib Require Import SetoidClass Morphisms PeanoNat. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Generalizable All Variables. diff --git a/src/Common/Gensym.v b/src/Common/Gensym.v index 1eaeb18dd..7fb9568ff 100644 --- a/src/Common/Gensym.v +++ b/src/Common/Gensym.v @@ -1,8 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Generate a symbol distinct from every element of a list of symbols *) (** Assumes a way to generate a new symbol from a pair of symbols "greater" than either one. *) -Require Import Coq.Classes.RelationClasses Coq.Lists.List Coq.ZArith.ZArith. -Require Import Coq.Strings.String Coq.Strings.Ascii. +From Stdlib Require Import RelationClasses List ZArith String Ascii. Require Import Fiat.Common.StringFacts. Set Implicit Arguments. diff --git a/src/Common/Instances.v b/src/Common/Instances.v index 44821bed0..f1f8c62da 100644 --- a/src/Common/Instances.v +++ b/src/Common/Instances.v @@ -1,4 +1,4 @@ -Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Program.Basics. +From Stdlib Require Import Setoid Morphisms RelationClasses Program.Basics. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Global Instance arrow2_1_Proper {A B RA RB X Y} diff --git a/src/Common/IterateBoundedIndex.v b/src/Common/IterateBoundedIndex.v index 63a99830b..ab24a2367 100644 --- a/src/Common/IterateBoundedIndex.v +++ b/src/Common/IterateBoundedIndex.v @@ -1,8 +1,5 @@ -Require Import Coq.Arith.Arith - Coq.Lists.List - Coq.Sets.Ensembles - Coq.Strings.String - Fiat.Common +From Stdlib Require Import Arith List Ensembles String. +Require Import Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.DecideableEnsembles. diff --git a/src/Common/Le.v b/src/Common/Le.v index 980bb9c12..750119245 100644 --- a/src/Common/Le.v +++ b/src/Common/Le.v @@ -1,8 +1,6 @@ (** * Common facts about [≤] *) Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Classes.Morphisms. -Require Import Coq.Program.Basics. +From Stdlib Require Import ZArith Morphisms Program.Basics. Set Implicit Arguments. diff --git a/src/Common/LetIn.v b/src/Common/LetIn.v index 64fb16b92..10b00604f 100644 --- a/src/Common/LetIn.v +++ b/src/Common/LetIn.v @@ -1,4 +1,4 @@ -Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions. +From Stdlib Require Import Morphisms Relation_Definitions. Require Import Fiat.Common.Tactics.GetGoal. Require Import Fiat.Common.Notations. diff --git a/src/Common/List/DisjointFacts.v b/src/Common/List/DisjointFacts.v index b753a7ab4..6e5a402d9 100644 --- a/src/Common/List/DisjointFacts.v +++ b/src/Common/List/DisjointFacts.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List. +From Stdlib Require Import List. Require Import Fiat.Common.List.Operations. Require Import Fiat.Common.List.ListFacts. diff --git a/src/Common/List/FlattenList.v b/src/Common/List/FlattenList.v index 5165f86b5..61f804685 100644 --- a/src/Common/List/FlattenList.v +++ b/src/Common/List/FlattenList.v @@ -1,6 +1,6 @@ -From Coq Require Import List SetoidList. +From Stdlib Require Import List SetoidList. Require Import Fiat.Common. -Require Import Coq.Arith.Arith. +From Stdlib Require Import Arith. Unset Implicit Arguments. diff --git a/src/Common/List/ListFacts.v b/src/Common/List/ListFacts.v index 01f969277..6d7ea223e 100644 --- a/src/Common/List/ListFacts.v +++ b/src/Common/List/ListFacts.v @@ -1,6 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.ZArith.ZArith. -From Coq Require Import List SetoidList Bool. +From Stdlib Require Import ZArith List SetoidList Bool. Require Import Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts. Unset Implicit Arguments. diff --git a/src/Common/List/ListMorphisms.v b/src/Common/List/ListMorphisms.v index 0d3569106..a95e9fd57 100644 --- a/src/Common/List/ListMorphisms.v +++ b/src/Common/List/ListMorphisms.v @@ -1,6 +1,4 @@ -Require Import Coq.Lists.List. -Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. -Require Import Coq.Sorting.Permutation. +From Stdlib Require Import List Setoid Morphisms Permutation. Require Import Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.List.ListFacts Fiat.Common.List.Operations diff --git a/src/Common/List/Operations.v b/src/Common/List/Operations.v index e3100b877..4a786b738 100644 --- a/src/Common/List/Operations.v +++ b/src/Common/List/Operations.v @@ -1,5 +1,5 @@ (** Useful list operations *) -Require Import Coq.Lists.List. +From Stdlib Require Import List. Require Import Fiat.Common.BoolFacts. Require Import Fiat.Common.Equality. diff --git a/src/Common/List/PermutationFacts.v b/src/Common/List/PermutationFacts.v index 5228065c4..10434246a 100644 --- a/src/Common/List/PermutationFacts.v +++ b/src/Common/List/PermutationFacts.v @@ -1,5 +1,7 @@ -Require Export Coq.Sorting.Permutation Fiat.Common. -Require Import Coq.Lists.List Fiat.Common.List.ListFacts. +From Stdlib Require Export Permutation. +Require Export Fiat.Common. +From Stdlib Require Import List. +Require Import Fiat.Common.List.ListFacts. Unset Implicit Arguments. @@ -190,7 +192,7 @@ Proof. repeat rewrite <- Permutation_middle; eauto. Qed. -Require Import Coq.Program.Program. +From Stdlib Require Import Program. Lemma permutation_map_cons : forall {A} {B} (f: B -> A) {x1 l2} {shuffled: list A}, @@ -220,7 +222,7 @@ Proof. apply Permutation_length_1 in H; congruence. Qed. -From Coq Require Import SetoidList. +From Stdlib Require Import SetoidList. Lemma InA_app_swap {A} eqA : Equivalence eqA diff --git a/src/Common/List/UpperBound.v b/src/Common/List/UpperBound.v index 085428dc0..c296cefa5 100644 --- a/src/Common/List/UpperBound.v +++ b/src/Common/List/UpperBound.v @@ -1,5 +1,5 @@ (* UpperBound of a list.*) -Require Import Coq.Lists.List Coq.Bool.Bool Fiat.Common Fiat.Computation.Core Fiat.Computation.Refinements.General. +Require Import Stdlib.Lists.List Stdlib.Bool.Bool Fiat.Common Fiat.Computation.Core Fiat.Computation.Refinements.General. Open Scope list_scope. diff --git a/src/Common/LogicFacts.v b/src/Common/LogicFacts.v index dbb392b30..02c4876fd 100644 --- a/src/Common/LogicFacts.v +++ b/src/Common/LogicFacts.v @@ -1,5 +1,5 @@ -Require Coq.Lists.List. -Require Import Coq.Program.Basics. +From Stdlib Require List. +From Stdlib Require Import Basics. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Section LogicFacts. diff --git a/src/Common/LogicMorphisms.v b/src/Common/LogicMorphisms.v index e81ee3fc4..a5edc8afc 100644 --- a/src/Common/LogicMorphisms.v +++ b/src/Common/LogicMorphisms.v @@ -1,4 +1,4 @@ -Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Program.Basics. +From Stdlib Require Import Setoid Morphisms Program.Basics. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Local Coercion is_true : bool >-> Sortclass. diff --git a/src/Common/MSetBoundedLattice.v b/src/Common/MSetBoundedLattice.v index b2daf6324..3fac17609 100644 --- a/src/Common/MSetBoundedLattice.v +++ b/src/Common/MSetBoundedLattice.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Export Coq.MSets.MSetInterface. -Require Import Coq.MSets.MSetFacts. -Require Import Coq.MSets.MSetProperties. +From Stdlib Require Export MSetInterface. +From Stdlib Require Import MSetFacts. +From Stdlib Require Import MSetProperties. Require Import Fiat.Common.Wf. Require Import Fiat.Common.LogicFacts. Require Import Fiat.Common.Instances. diff --git a/src/Common/MSetExtensions.v b/src/Common/MSetExtensions.v index b4ef399e2..c8991cb71 100644 --- a/src/Common/MSetExtensions.v +++ b/src/Common/MSetExtensions.v @@ -1,7 +1,4 @@ -Require Export Coq.MSets.MSetInterface. -Require Import Coq.MSets.MSetProperties - Coq.MSets.MSetFacts - Coq.MSets.MSetDecide. +From Stdlib Require Export MSetInterface MSetProperties MSetFacts MSetDecide. Require Import Fiat.Common.Instances. Require Import Fiat.Common.BoolFacts. Require Import Fiat.Common. diff --git a/src/Common/Monad.v b/src/Common/Monad.v index 1f0c575b6..18ac5b2cf 100644 --- a/src/Common/Monad.v +++ b/src/Common/Monad.v @@ -1,4 +1,4 @@ -Require Import Coq.Program.Program. +From Stdlib Require Import Program. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Set Implicit Arguments. diff --git a/src/Common/NatFacts.v b/src/Common/NatFacts.v index 724dfb4cd..108e364fa 100644 --- a/src/Common/NatFacts.v +++ b/src/Common/NatFacts.v @@ -1,6 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Classes.Morphisms. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import Morphisms ZArith. Lemma min_def {x y} : min x y = x - (x - y). Proof. apply Nat.min_case_strong; omega. Qed. diff --git a/src/Common/OptionFacts.v b/src/Common/OptionFacts.v index 61e90fb5a..e71f1c35c 100644 --- a/src/Common/OptionFacts.v +++ b/src/Common/OptionFacts.v @@ -1,4 +1,4 @@ -Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions. +From Stdlib Require Import Morphisms Relation_Definitions. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Set Implicit Arguments. diff --git a/src/Common/PointedProp.v b/src/Common/PointedProp.v index b720bd015..a55b69b1b 100644 --- a/src/Common/PointedProp.v +++ b/src/Common/PointedProp.v @@ -2,7 +2,7 @@ (** This allows for something between [bool] and [Prop], where we can computationally reduce things like [True /\ True], but can still express equality of types. *) -Require Import Coq.Setoids.Setoid. +From Stdlib Require Import Setoid. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Delimit Scope pointed_prop_scope with pointed_prop. diff --git a/src/Common/SetEq.v b/src/Common/SetEq.v index 66749f47a..ae4357f5b 100644 --- a/src/Common/SetEq.v +++ b/src/Common/SetEq.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Coq.Bool.Bool Coq.Structures.OrderedType Coq.Classes.Morphisms Coq.Setoids.Setoid. +From Stdlib Require Import List Bool OrderedType Morphisms Setoid. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Definition SetEq {A: Type} (seq1: list A) (seq2: list A) := diff --git a/src/Common/SetEqProperties.v b/src/Common/SetEqProperties.v index 6a16facc4..608333951 100644 --- a/src/Common/SetEqProperties.v +++ b/src/Common/SetEqProperties.v @@ -1,5 +1,5 @@ -Require Import Coq.Setoids.Setoid Coq.Lists.List Coq.Sorting.Permutation - Fiat.Common.List.FlattenList +From Stdlib Require Import Setoid List Permutation. +Require Import Fiat.Common.List.FlattenList Fiat.Common.SetEq. Definition IsSetEqSafe {A B: Type} (proc: list A -> list B) := diff --git a/src/Common/SetoidClassInstances.v b/src/Common/SetoidClassInstances.v index fcd7d3c2c..8e9747a90 100644 --- a/src/Common/SetoidClassInstances.v +++ b/src/Common/SetoidClassInstances.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.RelationClasses Coq.Classes.Morphisms. +From Stdlib Require Import List Setoid RelationClasses Morphisms. Require Import Fiat.Common.Tactics.SplitInContext. Set Implicit Arguments. diff --git a/src/Common/SetoidInstances.v b/src/Common/SetoidInstances.v index 5924b0900..f56ce9fdf 100644 --- a/src/Common/SetoidInstances.v +++ b/src/Common/SetoidInstances.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.RelationClasses Coq.Classes.Morphisms. +From Stdlib Require Import List Setoid RelationClasses Morphisms. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Set Implicit Arguments. diff --git a/src/Common/StringBound.v b/src/Common/StringBound.v index ac5eeecfc..cf2d18f14 100644 --- a/src/Common/StringBound.v +++ b/src/Common/StringBound.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Fiat.Common.ilist. +Require Import Stdlib.Lists.List Stdlib.Strings.String Stdlib.Arith.Arith Fiat.Common.ilist. Require Export Fiat.Common.BoundedLookup. (* Typeclasses for ensuring that a string is included in a list (i.e. a set of method names). This allows @@ -81,7 +81,7 @@ Require Export Fiat.Common.BoundedLookup. Variable A_eq_dec : forall a a' : A, {a = a'} + {a <> a'}. - Require Import Coq.Logic.Eqdep_dec. + Require Import Stdlib.Logic.Eqdep_dec. Program Definition Opt_A_eq_dec (a a' : option A): {a = a'} + {a <> a'} := diff --git a/src/Common/StringFacts.v b/src/Common/StringFacts.v index 10b7aca73..a81113163 100644 --- a/src/Common/StringFacts.v +++ b/src/Common/StringFacts.v @@ -1,8 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Arith.PeanoNat. -Require Import Coq.Strings.Ascii. -Require Import Coq.Strings.String. +From Stdlib Require Import ZArith PeanoNat Ascii String. Require Import Fiat.Common.List.Operations. Require Import Fiat.Common.StringOperations. diff --git a/src/Common/StringOperations.v b/src/Common/StringOperations.v index a6876e23f..32e48f3d2 100644 --- a/src/Common/StringOperations.v +++ b/src/Common/StringOperations.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Set Implicit Arguments. diff --git a/src/Common/String_as_OT.v b/src/Common/String_as_OT.v index 9a4e5b449..bd27f6292 100644 --- a/src/Common/String_as_OT.v +++ b/src/Common/String_as_OT.v @@ -1,5 +1,4 @@ -Require Import Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii. -Require Import Coq.Structures.OrderedType. +From Stdlib Require Import ZArith String Ascii OrderedType. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Lemma nat_compare_eq_refl : forall x, Nat.compare x x = Eq. @@ -194,7 +193,7 @@ End String_as_OT. (* Usage example: Require Import FMapAVL. -Require Import Coq.Structures.OrderedTypeEx. +Require Import Stdlib.Structures.OrderedTypeEx. Module StringIndexedMap := FMapAVL.Make(String_as_OT). Definition String2Nat := StringIndexedMap.t nat. diff --git a/src/Common/SumType.v b/src/Common/SumType.v index a34002078..35d6e6b34 100644 --- a/src/Common/SumType.v +++ b/src/Common/SumType.v @@ -1,6 +1,4 @@ -Require Import - Coq.Vectors.Vector - Coq.Vectors.Vector. +From Stdlib Require Import Vector. Require Import Fiat.Common.BoundedLookup. diff --git a/src/Common/Tactics/CacheStringConstant.v b/src/Common/Tactics/CacheStringConstant.v index ee19780f3..21e01754a 100644 --- a/src/Common/Tactics/CacheStringConstant.v +++ b/src/Common/Tactics/CacheStringConstant.v @@ -1,6 +1,5 @@ -Require Import - Coq.Strings.String - Fiat.Common.BoundedLookup +From Stdlib Require Import String. +Require Import Fiat.Common.BoundedLookup Fiat.Common.Tactics.HintDbExtra Fiat.Common.Tactics.TransparentAbstract. diff --git a/src/Common/Telescope/Core.v b/src/Common/Telescope/Core.v index 2f5642cb0..3475cf2a0 100644 --- a/src/Common/Telescope/Core.v +++ b/src/Common/Telescope/Core.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Relations.Relation_Definitions Coq.Classes.Morphisms. +From Stdlib Require Import Relation_Definitions Morphisms. Global Set Asymmetric Patterns. Module Export Telescope. diff --git a/src/Common/Telescope/Equality.v b/src/Common/Telescope/Equality.v index 9f76016bc..59562f1e4 100644 --- a/src/Common/Telescope/Equality.v +++ b/src/Common/Telescope/Equality.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Classes.Morphisms. +From Stdlib Require Import RelationClasses Relation_Definitions Morphisms. Require Import Fiat.Common.Equality. Require Import Fiat.Common.Telescope.Core. Require Import Fiat.Common.Telescope.Instances. diff --git a/src/Common/Telescope/Instances.v b/src/Common/Telescope/Instances.v index 576606549..cce6064ce 100644 --- a/src/Common/Telescope/Instances.v +++ b/src/Common/Telescope/Instances.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Classes.Morphisms. +From Stdlib Require Import RelationClasses Relation_Definitions Morphisms. Require Import Fiat.Common.Telescope.Core. Module Export Telescope. diff --git a/src/Common/UIP.v b/src/Common/UIP.v index a7eba091b..b95e0de1a 100644 --- a/src/Common/UIP.v +++ b/src/Common/UIP.v @@ -1,6 +1,6 @@ (** * Common facts about UIP and proof irrelevance *) -Require Coq.Strings.String. -Require Import Coq.Logic.EqdepFacts. +From Stdlib Require String. +From Stdlib Require Import EqdepFacts. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Set Implicit Arguments. diff --git a/src/Common/VectorFacts.v b/src/Common/VectorFacts.v index acb400f08..734286e0a 100644 --- a/src/Common/VectorFacts.v +++ b/src/Common/VectorFacts.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Coq.Vectors.Vector. +From Stdlib Require Vector. Import Vectors.Vector.VectorNotations. Set Implicit Arguments. diff --git a/src/Common/Wf.v b/src/Common/Wf.v index 0beffb173..05c974517 100644 --- a/src/Common/Wf.v +++ b/src/Common/Wf.v @@ -1,10 +1,10 @@ (** * Miscellaneous Well-Foundedness Facts *) -From Coq Require Import Setoid. -From Coq.Program Require Import Program Wf. -From Coq Require Import Wf_nat Morphisms. -From Coq.Init Require Import Wf. -From Coq Require Import SetoidList. -Require Import Coq.Arith.PeanoNat. +From Stdlib Require Import Setoid. +From Stdlib.Program Require Import Program Wf. +From Stdlib Require Import Wf_nat Morphisms. +From Stdlib Require Import Init.Wf. +From Stdlib Require Import SetoidList. +From Stdlib Require Import PeanoNat. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Set Implicit Arguments. diff --git a/src/Common/Wf1.v b/src/Common/Wf1.v index a94dc65b9..e188f76ca 100644 --- a/src/Common/Wf1.v +++ b/src/Common/Wf1.v @@ -1,6 +1,6 @@ (** * Miscellaneous Well-Foundedness Facts *) Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf. +From Stdlib Require Import Setoid Program Program.Wf Wf_nat Morphisms Init.Wf. Require Import Fiat.Common.Telescope.Core. Require Import Fiat.Common.Telescope.Instances. Require Import Fiat.Common.Telescope.Equality. diff --git a/src/Common/Wf2.v b/src/Common/Wf2.v index 597adb8a5..68f04c56e 100644 --- a/src/Common/Wf2.v +++ b/src/Common/Wf2.v @@ -1,6 +1,6 @@ (** * Miscellaneous Well-Foundedness Facts *) Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf. +Require Import Stdlib.Setoids.Setoid Stdlib.Program.Program Stdlib.Program.Wf Stdlib.Arith.Wf_nat Stdlib.Classes.Morphisms Stdlib.Init.Wf. Require Import Fiat.Common.Telescope.Core. Require Import Fiat.Common.Telescope.Instances. Require Import Fiat.Common.Telescope.Equality. diff --git a/src/Common/i2list.v b/src/Common/i2list.v index bdb207897..9a7590283 100644 --- a/src/Common/i2list.v +++ b/src/Common/i2list.v @@ -1,8 +1,8 @@ Generalizable All Variables. Set Implicit Arguments. -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common.ilist2. diff --git a/src/Common/i2list2.v b/src/Common/i2list2.v index ddf2c4fad..c75c34185 100644 --- a/src/Common/i2list2.v +++ b/src/Common/i2list2.v @@ -1,11 +1,8 @@ Generalizable All Variables. Set Implicit Arguments. -Require Import - Coq.Lists.List - Coq.Strings.String - Coq.Arith.Arith - Fiat.Common.ilist +From Stdlib Require Import List String Arith. +Require Import Fiat.Common.ilist Fiat.Common.ilist2. Section i2list2. diff --git a/src/Common/i3list.v b/src/Common/i3list.v index e7e8636ac..95b5cce3f 100644 --- a/src/Common/i3list.v +++ b/src/Common/i3list.v @@ -1,10 +1,8 @@ Generalizable All Variables. Set Implicit Arguments. -Require Import Coq.Lists.List - Coq.Strings.String - Coq.Arith.Arith - Fiat.Common.ilist +From Stdlib Require Import List String Arith. +Require Import Fiat.Common.ilist Fiat.Common.ilist3. Section i3list. diff --git a/src/Common/i3list2.v b/src/Common/i3list2.v index b117fa76a..6ff6dd106 100644 --- a/src/Common/i3list2.v +++ b/src/Common/i3list2.v @@ -1,10 +1,8 @@ Generalizable All Variables. Set Implicit Arguments. -Require Import Coq.Lists.List - Coq.Strings.String - Coq.Arith.Arith - Fiat.Common.ilist +From Stdlib Require Import List String Arith. +Require Import Fiat.Common.ilist Fiat.Common.ilist3. Section i3list2. diff --git a/src/Common/ilist.v b/src/Common/ilist.v index c274c1bf2..0c4e1cf48 100644 --- a/src/Common/ilist.v +++ b/src/Common/ilist.v @@ -1,12 +1,10 @@ Generalizable All Variables. Set Implicit Arguments. -Require Import Coq.Lists.List - Coq.Strings.String - Coq.Arith.Arith - Fiat.Common. +From Stdlib Require Import List String Arith. +Require Import Fiat.Common. Require Export Fiat.Common.VectorFacts. -Require Coq.Vectors.Vector. +From Stdlib Require Vector. Section ilist. diff --git a/src/Common/ilist2.v b/src/Common/ilist2.v index 25e9f2951..924ff0891 100644 --- a/src/Common/ilist2.v +++ b/src/Common/ilist2.v @@ -1,7 +1,7 @@ Generalizable All Variables. Set Implicit Arguments. -Require Import Coq.Lists.List Coq.Strings.String Coq.Arith.Arith. +From Stdlib Require Import List String Arith. Require Import Fiat.Common.ilist. Require Import Fiat.Common. Require Export Fiat.Common.VectorFacts. diff --git a/src/Common/ilist2_pair.v b/src/Common/ilist2_pair.v index 9090cd1fd..e0edabca3 100644 --- a/src/Common/ilist2_pair.v +++ b/src/Common/ilist2_pair.v @@ -1,8 +1,8 @@ Generalizable All Variables. Set Implicit Arguments. -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Arith.Arith Fiat.Common.ilist Fiat.Common.ilist2. diff --git a/src/Common/ilist3.v b/src/Common/ilist3.v index cc3655594..1311221dc 100644 --- a/src/Common/ilist3.v +++ b/src/Common/ilist3.v @@ -1,7 +1,7 @@ Generalizable All Variables. Set Implicit Arguments. -Require Import Coq.Lists.List Coq.Strings.String Coq.Arith.Arith. +From Stdlib Require Import List String Arith. Require Import Fiat.Common.ilist. Require Import Fiat.Common. diff --git a/src/Common/ilist3_pair.v b/src/Common/ilist3_pair.v index 6973b8485..3d109550b 100644 --- a/src/Common/ilist3_pair.v +++ b/src/Common/ilist3_pair.v @@ -1,11 +1,8 @@ Generalizable All Variables. Set Implicit Arguments. -Require Import Coq.Lists.List - Coq.Strings.String - Coq.Arith.Arith - Fiat.Common.ilist - Fiat.Common.ilist3. +From Stdlib Require Import List String Arith. +Require Import Fiat.Common.ilist Fiat.Common.ilist3. Section ilist3_pair. diff --git a/src/Computation/ApplyMonad.v b/src/Computation/ApplyMonad.v index 20261761d..2adf25cbe 100644 --- a/src/Computation/ApplyMonad.v +++ b/src/Computation/ApplyMonad.v @@ -1,5 +1,5 @@ (** * A variant of the [Comp] monad laws using [apply] *) -Require Import Coq.Strings.String Coq.Sets.Ensembles. +From Stdlib Require Import String Ensembles. Require Import Fiat.Common. Require Import Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.SetoidMorphisms. diff --git a/src/Computation/Core.v b/src/Computation/Core.v index 5de407645..145a7df6a 100644 --- a/src/Computation/Core.v +++ b/src/Computation/Core.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.Sets.Ensembles. +From Stdlib Require Import String Ensembles. Require Import Fiat.Common. Require Export Fiat.Computation.Notations. diff --git a/src/Computation/Decidable.v b/src/Computation/Decidable.v index 9bfaf7d58..cebc22ecd 100644 --- a/src/Computation/Decidable.v +++ b/src/Computation/Decidable.v @@ -1,4 +1,4 @@ -Require Import Coq.Arith.Compare_dec. +From Stdlib Require Import Compare_dec. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Generalizable All Variables. @@ -131,15 +131,15 @@ End DecidableLogic. Local Ltac t' tac := t; apply tac; assumption. -Require Import Coq.Bool.Bool. +From Stdlib Require Import Bool. Global Program Instance bool_eq_Decidable {n m : bool} : Decidable (n = m) := { Decidable_witness := eqb n m }. Obligation 1. t' eqb_true_iff. Qed. -Require Import Coq.Strings.Ascii. -From Coq Require Import Sumbool. +Require Import Stdlib.Strings.Ascii. +From Stdlib Require Import Sumbool. Global Program Instance ascii_eq_Decidable {n m : Ascii.ascii} : Decidable (n = m) := { @@ -147,7 +147,7 @@ Global Program Instance ascii_eq_Decidable {n m : Ascii.ascii} : }. Obligation 1. t; destruct (Ascii.ascii_dec n m); auto; discriminate. Qed. -Require Import Coq.Arith.Arith. +Require Import Stdlib.Arith.Arith. Global Program Instance nat_eq_Decidable {n m : nat} : Decidable (n = m) := { Decidable_witness := Nat.eqb n m @@ -161,7 +161,7 @@ Obligation 1. t' leb_iff. Qed. Global Instance lt_Decidable {n m} : Decidable (lt n m) := le_Decidable. -Require Import Coq.NArith.NArith. +Require Import Stdlib.NArith.NArith. Global Program Instance N_eq_Decidable {n m : N} : Decidable (n = m) := { Decidable_witness := N.eqb n m @@ -178,7 +178,7 @@ Global Program Instance Nlt_Decidable {n m} : Decidable (N.lt n m) := { }. Obligation 1. t' N.ltb_lt. Qed. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Global Program Instance Z_eq_Decidable {n m : Z} : Decidable (n = m) := { Decidable_witness := Z.eqb n m @@ -195,7 +195,7 @@ Global Program Instance Zlt_Decidable {n m} : Decidable (Z.lt n m) := { }. Obligation 1. t' Z.ltb_lt. Qed. -Require Import Coq.QArith.QArith. +Require Import Stdlib.QArith.QArith. Global Program Instance Q_eq_Decidable {n m : Q} : Decidable (n == m) := { Decidable_witness := Qeq_bool n m diff --git a/src/Computation/FixComp.v b/src/Computation/FixComp.v index 6ceeac3ff..f9d1dd2ec 100644 --- a/src/Computation/FixComp.v +++ b/src/Computation/FixComp.v @@ -1,12 +1,8 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import - Coq.Sets.Ensembles - Coq.ZArith.ZArith - Coq.Classes.Morphisms - Coq.Classes.SetoidTactics - Fiat.Computation - Fiat.Computation.SetoidMorphisms - Coq.Logic.FunctionalExtensionality. +From Stdlib Require Import Ensembles ZArith Morphisms SetoidTactics. +Require Import Fiat.Computation + Fiat.Computation.SetoidMorphisms. +From Stdlib Require Import FunctionalExtensionality. Require Fiat.Common.Frame. Require Fiat.Common. diff --git a/src/Computation/FoldComp.v b/src/Computation/FoldComp.v index c6123f1be..8b2b52827 100644 --- a/src/Computation/FoldComp.v +++ b/src/Computation/FoldComp.v @@ -109,7 +109,7 @@ Proof. apply IHxs. Qed. -Require Import Coq.Lists.List. +From Stdlib Require Import List. Lemma refine_foldComp_fold_left_helper : forall A (xs : list A) S (f : S -> A -> Comp S) (z : Comp S), diff --git a/src/Computation/FueledFix.v b/src/Computation/FueledFix.v index ec04f5dba..592c2b7aa 100644 --- a/src/Computation/FueledFix.v +++ b/src/Computation/FueledFix.v @@ -1,5 +1,4 @@ -Require Import Coq.Classes.Morphisms - Coq.Classes.SetoidTactics. +From Stdlib Require Import Morphisms SetoidTactics. Require Import Fiat.Computation. Section FueledFix. diff --git a/src/Computation/ListComputations.v b/src/Computation/ListComputations.v index 110c22dab..7f0dedaee 100644 --- a/src/Computation/ListComputations.v +++ b/src/Computation/ListComputations.v @@ -1,7 +1,4 @@ -Require Import - Coq.Arith.Arith - Coq.Sets.Ensembles - Coq.Lists.List. +From Stdlib Require Import Arith Ensembles List. Require Import Fiat.Common.List.ListFacts diff --git a/src/Computation/LogicLemmas.v b/src/Computation/LogicLemmas.v index fc8ce7588..3e8812380 100644 --- a/src/Computation/LogicLemmas.v +++ b/src/Computation/LogicLemmas.v @@ -1,4 +1,4 @@ -Require Import Coq.Program.Program. +From Stdlib Require Import Program. Require Import Fiat.Common. (** * Various useful lemmas about logic *) diff --git a/src/Computation/Monad.v b/src/Computation/Monad.v index ab5c73279..26af994b4 100644 --- a/src/Computation/Monad.v +++ b/src/Computation/Monad.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.Sets.Ensembles. +From Stdlib Require Import String Ensembles. Require Import Fiat.Common. Require Import Fiat.Computation.Core. diff --git a/src/Computation/Refinements/General.v b/src/Computation/Refinements/General.v index c1cc12e73..2251ec244 100644 --- a/src/Computation/Refinements/General.v +++ b/src/Computation/Refinements/General.v @@ -1,6 +1,4 @@ -Require Import Coq.Strings.String - Coq.Sets.Ensembles - Coq.Bool.Bool. +From Stdlib Require Import String Ensembles Bool. Require Import Fiat.Common Fiat.Common.BoolFacts Fiat.Common.LogicFacts diff --git a/src/Computation/Refinements/Iterate_Decide_Comp.v b/src/Computation/Refinements/Iterate_Decide_Comp.v index 7304d302e..b772748d5 100644 --- a/src/Computation/Refinements/Iterate_Decide_Comp.v +++ b/src/Computation/Refinements/Iterate_Decide_Comp.v @@ -1,11 +1,5 @@ -Require Import - Coq.Lists.List - Coq.Arith.Compare_dec - Coq.Arith.Arith - Coq.Bool.Bool - Coq.Strings.String - Coq.Sets.Ensembles - Fiat.Common.BoolFacts +From Stdlib Require Import List Compare_dec Arith Bool String Ensembles. +Require Import Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.Common.IterateBoundedIndex diff --git a/src/Computation/SetoidEqMorphisms.v b/src/Computation/SetoidEqMorphisms.v index 0f7463bc2..42a3deae2 100644 --- a/src/Computation/SetoidEqMorphisms.v +++ b/src/Computation/SetoidEqMorphisms.v @@ -1,4 +1,4 @@ -Require Import Coq.Classes.Morphisms. +Require Import Stdlib.Classes.Morphisms. Require Import Fiat.Computation.Core. Global Instance ret_Proper_eq {A} diff --git a/src/Computation/SetoidMorphisms.v b/src/Computation/SetoidMorphisms.v index 5b464305a..6e550a559 100644 --- a/src/Computation/SetoidMorphisms.v +++ b/src/Computation/SetoidMorphisms.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List. +From Stdlib Require Import List. Require Import Fiat.Common. Require Import Fiat.Computation.Core. Require Import Fiat.Computation.Monad. diff --git a/src/ComputationalEnsembles/Core.v b/src/ComputationalEnsembles/Core.v index c9b221dcc..b80a5047f 100644 --- a/src/ComputationalEnsembles/Core.v +++ b/src/ComputationalEnsembles/Core.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Coq.Sets.Ensembles. +Require Import Stdlib.Lists.List Stdlib.Sets.Ensembles. Require Import Fiat.Computation.Core Fiat.Computation.Notations Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.Ensembles.Cardinal. diff --git a/src/ComputationalEnsembles/Laws.v b/src/ComputationalEnsembles/Laws.v index e52515a8e..a266b839f 100644 --- a/src/ComputationalEnsembles/Laws.v +++ b/src/ComputationalEnsembles/Laws.v @@ -1,4 +1,4 @@ -Require Import Coq.Classes.Morphisms Coq.Lists.List. +Require Import Stdlib.Classes.Morphisms Stdlib.Lists.List. Require Import Fiat.ComputationalEnsembles.Core Fiat.Computation. Require Import Fiat.Common.Ensembles.Tactics Fiat.Common.Ensembles. diff --git a/src/ComputationalEnsembles/Morphisms.v b/src/ComputationalEnsembles/Morphisms.v index f347b5576..64c16df79 100644 --- a/src/ComputationalEnsembles/Morphisms.v +++ b/src/ComputationalEnsembles/Morphisms.v @@ -1,4 +1,4 @@ -Require Import Coq.Sets.Ensembles. +From Stdlib Require Import Ensembles. Require Import Fiat.Computation Fiat.Common.Ensembles Fiat.ComputationalEnsembles.Core Fiat.ComputationalEnsembles.Laws. Require Import Fiat.Common. diff --git a/src/Examples/CacheADT/CacheADT.v b/src/Examples/CacheADT/CacheADT.v index fc4d772f7..676c3c6e9 100644 --- a/src/Examples/CacheADT/CacheADT.v +++ b/src/Examples/CacheADT/CacheADT.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles +From Stdlib Require Import String ZArith List FunctionalExtensionality Ensembles Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements. Open Scope string_scope. diff --git a/src/Examples/CacheADT/CacheRefinements.v b/src/Examples/CacheADT/CacheRefinements.v index 2b55b5b3a..de680142f 100644 --- a/src/Examples/CacheADT/CacheRefinements.v +++ b/src/Examples/CacheADT/CacheRefinements.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles +From Stdlib Require Import String ZArith List FunctionalExtensionality Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec. diff --git a/src/Examples/CacheADT/CacheSig.v b/src/Examples/CacheADT/CacheSig.v index 5a2e80c89..7138ef377 100644 --- a/src/Examples/CacheADT/CacheSig.v +++ b/src/Examples/CacheADT/CacheSig.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles +From Stdlib Require Import String ZArith List FunctionalExtensionality Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles. diff --git a/src/Examples/CacheADT/CacheSpec.v b/src/Examples/CacheADT/CacheSpec.v index d2015b74e..c315c0a98 100644 --- a/src/Examples/CacheADT/CacheSpec.v +++ b/src/Examples/CacheADT/CacheSpec.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles +From Stdlib Require Import String ZArith List FunctionalExtensionality Ensembles Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements Examples.CacheADT.KVEnsembles. diff --git a/src/Examples/CacheADT/FMapCacheImplementation.v b/src/Examples/CacheADT/FMapCacheImplementation.v index ec9c7c356..afec6c465 100644 --- a/src/Examples/CacheADT/FMapCacheImplementation.v +++ b/src/Examples/CacheADT/FMapCacheImplementation.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles +From Stdlib Require Import String ZArith List FunctionalExtensionality Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec CacheRefinements. diff --git a/src/Examples/CacheADT/KVEnsembles.v b/src/Examples/CacheADT/KVEnsembles.v index 9874e44c3..e24123f67 100644 --- a/src/Examples/CacheADT/KVEnsembles.v +++ b/src/Examples/CacheADT/KVEnsembles.v @@ -1,4 +1,4 @@ -Require Import Coq.Sets.Ensembles. +From Stdlib Require Import Ensembles. (* Definitions of basic operations on Ensembles of Key/Value pairs. *) diff --git a/src/Examples/CacheADT/LRUCache.v b/src/Examples/CacheADT/LRUCache.v index 59d5a207b..c67869337 100644 --- a/src/Examples/CacheADT/LRUCache.v +++ b/src/Examples/CacheADT/LRUCache.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles +From Stdlib Require Import String ZArith List FunctionalExtensionality Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec CacheRefinements FMapCacheImplementation. diff --git a/src/Examples/DnsServer/AuthoritativeDNSSchema.v b/src/Examples/DnsServer/AuthoritativeDNSSchema.v index 2dc04c19c..2e344e6e8 100644 --- a/src/Examples/DnsServer/AuthoritativeDNSSchema.v +++ b/src/Examples/DnsServer/AuthoritativeDNSSchema.v @@ -1,4 +1,4 @@ -Require Import Coq.Vectors.Vector +Require Import Stdlib.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector diff --git a/src/Examples/DnsServer/AuthoritativeDNSServer.v b/src/Examples/DnsServer/AuthoritativeDNSServer.v index 6c1b2d1b7..aad724730 100644 --- a/src/Examples/DnsServer/AuthoritativeDNSServer.v +++ b/src/Examples/DnsServer/AuthoritativeDNSServer.v @@ -1,4 +1,4 @@ -Require Import Coq.Vectors.Vector +Require Import Stdlib.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List. diff --git a/src/Examples/DnsServer/DnsLemmas.v b/src/Examples/DnsServer/DnsLemmas.v index 5be1906d0..40aa19c52 100644 --- a/src/Examples/DnsServer/DnsLemmas.v +++ b/src/Examples/DnsServer/DnsLemmas.v @@ -1,4 +1,4 @@ -Require Import Coq.Vectors.Vector +Require Import Stdlib.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector diff --git a/src/Examples/DnsServer/MinimalDNSServer.v b/src/Examples/DnsServer/MinimalDNSServer.v index 70d670784..b503a7054 100644 --- a/src/Examples/DnsServer/MinimalDNSServer.v +++ b/src/Examples/DnsServer/MinimalDNSServer.v @@ -1,4 +1,4 @@ -Require Import Coq.Vectors.Vector +Require Import Stdlib.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List. diff --git a/src/Examples/DnsServer/SimpleAuthoritativeDNSSchema.v b/src/Examples/DnsServer/SimpleAuthoritativeDNSSchema.v index a6017702a..a1a188c6e 100644 --- a/src/Examples/DnsServer/SimpleAuthoritativeDNSSchema.v +++ b/src/Examples/DnsServer/SimpleAuthoritativeDNSSchema.v @@ -1,4 +1,4 @@ -Require Import Coq.Vectors.Vector +Require Import Stdlib.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector diff --git a/src/Examples/DnsServer/SimpleDnsLemmas.v b/src/Examples/DnsServer/SimpleDnsLemmas.v index eb3edd808..c98a5997d 100644 --- a/src/Examples/DnsServer/SimpleDnsLemmas.v +++ b/src/Examples/DnsServer/SimpleDnsLemmas.v @@ -1,4 +1,4 @@ -Require Import Coq.Vectors.Vector +Require Import Stdlib.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector diff --git a/src/Examples/DnsServer/SimplifiedAuthoritativeDNSServer.v b/src/Examples/DnsServer/SimplifiedAuthoritativeDNSServer.v index 06d8c872d..6fa28c1be 100644 --- a/src/Examples/DnsServer/SimplifiedAuthoritativeDNSServer.v +++ b/src/Examples/DnsServer/SimplifiedAuthoritativeDNSServer.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Vectors.Vector +Require Import Stdlib.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List. diff --git a/src/Examples/HACMSDemo/HACMSDemo.v b/src/Examples/HACMSDemo/HACMSDemo.v index 8f2e69a30..00183ff97 100644 --- a/src/Examples/HACMSDemo/HACMSDemo.v +++ b/src/Examples/HACMSDemo/HACMSDemo.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Strings.Ascii +Require Import Stdlib.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Coq.Structures.OrderedType. diff --git a/src/Examples/HACMSDemo/WheelSensor.v b/src/Examples/HACMSDemo/WheelSensor.v index 542374270..474d524ed 100644 --- a/src/Examples/HACMSDemo/WheelSensor.v +++ b/src/Examples/HACMSDemo/WheelSensor.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.Ascii +Require Import Stdlib.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Coq.Structures.OrderedType. diff --git a/src/Examples/HACMSDemo/WheelSensorDecoder.v b/src/Examples/HACMSDemo/WheelSensorDecoder.v index 7e9e565d0..24dd7e677 100644 --- a/src/Examples/HACMSDemo/WheelSensorDecoder.v +++ b/src/Examples/HACMSDemo/WheelSensorDecoder.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.Ascii +Require Import Stdlib.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Coq.Structures.OrderedType. diff --git a/src/Examples/HACMSDemo/WheelSensorEncoder.v b/src/Examples/HACMSDemo/WheelSensorEncoder.v index 9acbbc703..a362742ec 100644 --- a/src/Examples/HACMSDemo/WheelSensorEncoder.v +++ b/src/Examples/HACMSDemo/WheelSensorEncoder.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.Ascii +Require Import Stdlib.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Coq.Structures.OrderedType. diff --git a/src/Examples/HACMSDemo/WheelSensorExtraction.v b/src/Examples/HACMSDemo/WheelSensorExtraction.v index 94bd05d3d..a51165db9 100644 --- a/src/Examples/HACMSDemo/WheelSensorExtraction.v +++ b/src/Examples/HACMSDemo/WheelSensorExtraction.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.Ascii +Require Import Stdlib.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Coq.Structures.OrderedType. @@ -34,7 +34,7 @@ Require Import Require Import Bedrock.Word. -Require Import Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatInt Coq.extraction.ExtrOcamlZInt Coq.extraction.ExtrOcamlString. +Require Import Stdlib.extraction.ExtrOcamlBasic Stdlib.extraction.ExtrOcamlNatInt Stdlib.extraction.ExtrOcamlZInt Stdlib.extraction.ExtrOcamlString. Extract Inductive bool => bool [ true false ]. Extract Inductive list => "list" [ "[]" "(::)" ]. diff --git a/src/Examples/Ics/Ics.v b/src/Examples/Ics/Ics.v index be4c66503..f242a3f5b 100644 --- a/src/Examples/Ics/Ics.v +++ b/src/Examples/Ics/Ics.v @@ -7,7 +7,7 @@ Require Import Fiat.ADT.ComputationalADT. Require Import Fiat.ADTRefinement.GeneralBuildADTRefinements. Require Import Fiat.ADT.ComputationalADT Fiat.ADTRefinement.GeneralBuildADTRefinements. -Require Import Coq.Bool.Bool Coq.ZArith.ZArith. +Require Import Stdlib.Bool.Bool Stdlib.ZArith.ZArith. Export ADTNotation.BuildADT ADTNotation.BuildComputationalADT ADTNotation.BuildADTSig. Export ADTRefinement.GeneralRefinements ADT.ComputationalADT Core. diff --git a/src/Examples/QueryStructure/BookstoreOcaml.v b/src/Examples/QueryStructure/BookstoreOcaml.v index 5a193bb6b..474659ea7 100644 --- a/src/Examples/QueryStructure/BookstoreOcaml.v +++ b/src/Examples/QueryStructure/BookstoreOcaml.v @@ -5,8 +5,8 @@ Time Definition BookstoreImpl : ComputationalADT.cADT BookStoreSig := Eval simpl in projT1 SharpenedBookStore. Require Import Fiat.Computation.Core Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements. -Require Import Fiat.Common.String_as_OT Coq.Structures.OrderedTypeEx. -Require Import Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatInt Coq.extraction.ExtrOcamlZInt Coq.extraction.ExtrOcamlString. +Require Import Fiat.Common.String_as_OT Stdlib.Structures.OrderedTypeEx. +Require Import Stdlib.extraction.ExtrOcamlBasic Stdlib.extraction.ExtrOcamlNatInt Stdlib.extraction.ExtrOcamlZInt Stdlib.extraction.ExtrOcamlString. Extract Inlined Constant fst => fst. Extract Inlined Constant snd => snd. diff --git a/src/Examples/QueryStructure/ClassifierExtraction.v b/src/Examples/QueryStructure/ClassifierExtraction.v index 4cdc412f7..a95a5a412 100644 --- a/src/Examples/QueryStructure/ClassifierExtraction.v +++ b/src/Examples/QueryStructure/ClassifierExtraction.v @@ -1,5 +1,5 @@ -Require Import Coq.Bool.Bool Coq.Strings.String Fiat.Common.String_as_OT Coq.Structures.OrderedTypeEx. -Require Import Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatInt Coq.extraction.ExtrOcamlZInt Coq.extraction.ExtrOcamlString. +Require Import Stdlib.Bool.Bool Stdlib.Strings.String Fiat.Common.String_as_OT Stdlib.Structures.OrderedTypeEx. +Require Import Stdlib.extraction.ExtrOcamlBasic Stdlib.extraction.ExtrOcamlNatInt Stdlib.extraction.ExtrOcamlZInt Stdlib.extraction.ExtrOcamlString. Require Import Fiat.QueryStructure.Automation.MasterPlan Fiat.Examples.QueryStructure.Classifier. diff --git a/src/Examples/QueryStructure/ClassifierUnOptExtraction.v b/src/Examples/QueryStructure/ClassifierUnOptExtraction.v index 1f22965c1..94e8c5c86 100644 --- a/src/Examples/QueryStructure/ClassifierUnOptExtraction.v +++ b/src/Examples/QueryStructure/ClassifierUnOptExtraction.v @@ -1,5 +1,5 @@ -Require Import Coq.Bool.Bool Coq.Strings.String Fiat.Common.String_as_OT Coq.Structures.OrderedTypeEx. -Require Import Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatInt Coq.extraction.ExtrOcamlZInt Coq.extraction.ExtrOcamlString. +Require Import Stdlib.Bool.Bool Stdlib.Strings.String Fiat.Common.String_as_OT Stdlib.Structures.OrderedTypeEx. +Require Import Stdlib.extraction.ExtrOcamlBasic Stdlib.extraction.ExtrOcamlNatInt Stdlib.extraction.ExtrOcamlZInt Stdlib.extraction.ExtrOcamlString. Require Import Fiat.QueryStructure.Automation.MasterPlan Fiat.Examples.QueryStructure.ClassifierUnOpt. diff --git a/src/Examples/QueryStructure/MessagesExtraction.v b/src/Examples/QueryStructure/MessagesExtraction.v index 01ab92d61..791b48906 100644 --- a/src/Examples/QueryStructure/MessagesExtraction.v +++ b/src/Examples/QueryStructure/MessagesExtraction.v @@ -1,5 +1,5 @@ -Require Import Coq.Bool.Bool Coq.Strings.String Fiat.Common.String_as_OT Coq.Structures.OrderedTypeEx. -Require Import Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatInt Coq.extraction.ExtrOcamlZInt Coq.extraction.ExtrOcamlString. +Require Import Stdlib.Bool.Bool Stdlib.Strings.String Fiat.Common.String_as_OT Stdlib.Structures.OrderedTypeEx. +Require Import Stdlib.extraction.ExtrOcamlBasic Stdlib.extraction.ExtrOcamlNatInt Stdlib.extraction.ExtrOcamlZInt Stdlib.extraction.ExtrOcamlString. Require Import Fiat.QueryStructure.Automation.MasterPlan Fiat.Examples.QueryStructure.Messages. diff --git a/src/Examples/QueryStructure/PhotoalbumExtraction.v b/src/Examples/QueryStructure/PhotoalbumExtraction.v index 610f40bbf..ec402d632 100644 --- a/src/Examples/QueryStructure/PhotoalbumExtraction.v +++ b/src/Examples/QueryStructure/PhotoalbumExtraction.v @@ -1,5 +1,5 @@ -Require Import Coq.Bool.Bool Coq.Strings.String Fiat.Common.String_as_OT Coq.Structures.OrderedTypeEx. -Require Import Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatInt Coq.extraction.ExtrOcamlZInt Coq.extraction.ExtrOcamlString. +Require Import Stdlib.Bool.Bool Stdlib.Strings.String Fiat.Common.String_as_OT Stdlib.Structures.OrderedTypeEx. +Require Import Stdlib.extraction.ExtrOcamlBasic Stdlib.extraction.ExtrOcamlNatInt Stdlib.extraction.ExtrOcamlZInt Stdlib.extraction.ExtrOcamlString. Require Import Fiat.QueryStructure.Automation.MasterPlan Fiat.Examples.QueryStructure.Photoalbum. diff --git a/src/Examples/QueryStructure/PhotoalbumUnOptimizedExtraction.v b/src/Examples/QueryStructure/PhotoalbumUnOptimizedExtraction.v index fba2df5f7..5859a63ac 100644 --- a/src/Examples/QueryStructure/PhotoalbumUnOptimizedExtraction.v +++ b/src/Examples/QueryStructure/PhotoalbumUnOptimizedExtraction.v @@ -1,5 +1,5 @@ -Require Import Coq.Bool.Bool Coq.Strings.String Fiat.Common.String_as_OT Coq.Structures.OrderedTypeEx. -Require Import Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatInt Coq.extraction.ExtrOcamlZInt Coq.extraction.ExtrOcamlString. +Require Import Stdlib.Bool.Bool Stdlib.Strings.String Fiat.Common.String_as_OT Stdlib.Structures.OrderedTypeEx. +Require Import Stdlib.extraction.ExtrOcamlBasic Stdlib.extraction.ExtrOcamlNatInt Stdlib.extraction.ExtrOcamlZInt Stdlib.extraction.ExtrOcamlString. Require Import Fiat.QueryStructure.Automation.MasterPlan Fiat.Examples.QueryStructure.PhotoalbumUnOpt. diff --git a/src/Examples/Tutorial/NotInList.v b/src/Examples/Tutorial/NotInList.v index 129d4b9b4..b9615caaa 100644 --- a/src/Examples/Tutorial/NotInList.v +++ b/src/Examples/Tutorial/NotInList.v @@ -1,9 +1,9 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Strings.Ascii +Require Import Stdlib.Strings.Ascii Coq.Bool.Bool Coq.Lists.List. -Require Export Coq.Vectors.Vector +Require Export Stdlib.Vectors.Vector Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Bool.Bool diff --git a/src/Examples/Tutorial/Tutorial.v b/src/Examples/Tutorial/Tutorial.v index f1a8d97d2..423c4553b 100644 --- a/src/Examples/Tutorial/Tutorial.v +++ b/src/Examples/Tutorial/Tutorial.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Strings.Ascii +Require Import Stdlib.Strings.Ascii Coq.Bool.Bool Coq.Lists.List. @@ -9,7 +9,7 @@ Require Import Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms. -Export Coq.Vectors.Vector +Export Stdlib.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector diff --git a/src/Fiat4Monitors/HealthMonitor/HealthMonitorSpec.v b/src/Fiat4Monitors/HealthMonitor/HealthMonitorSpec.v index e0a5dc349..0c3060595 100644 --- a/src/Fiat4Monitors/HealthMonitor/HealthMonitorSpec.v +++ b/src/Fiat4Monitors/HealthMonitor/HealthMonitorSpec.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Program.Program diff --git a/src/Fiat4Monitors/HealthMonitor/HealthMonitors.v b/src/Fiat4Monitors/HealthMonitor/HealthMonitors.v index 3a86b5327..a750b7102 100644 --- a/src/Fiat4Monitors/HealthMonitor/HealthMonitors.v +++ b/src/Fiat4Monitors/HealthMonitor/HealthMonitors.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Program.Program diff --git a/src/Fiat4Monitors/LandsharkNodes.v b/src/Fiat4Monitors/LandsharkNodes.v index 17a5592cf..bd646f6d6 100644 --- a/src/Fiat4Monitors/LandsharkNodes.v +++ b/src/Fiat4Monitors/LandsharkNodes.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Program.Program diff --git a/src/Fiat4Monitors/LandsharkTopics.v b/src/Fiat4Monitors/LandsharkTopics.v index 0e637ee6e..50f55e236 100644 --- a/src/Fiat4Monitors/LandsharkTopics.v +++ b/src/Fiat4Monitors/LandsharkTopics.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Program.Program diff --git a/src/Fiat4Monitors/MonitorRepInv.v b/src/Fiat4Monitors/MonitorRepInv.v index 21ddad3d9..997bee186 100644 --- a/src/Fiat4Monitors/MonitorRepInv.v +++ b/src/Fiat4Monitors/MonitorRepInv.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List +Require Import Stdlib.Lists.List Coq.Program.Program Coq.Arith.Arith. Require Import diff --git a/src/Fiat4Monitors/RADLMNodeADTs.v b/src/Fiat4Monitors/RADLMNodeADTs.v index c49520b7f..0136db878 100644 --- a/src/Fiat4Monitors/RADLMNodeADTs.v +++ b/src/Fiat4Monitors/RADLMNodeADTs.v @@ -1,9 +1,9 @@ Set Implicit Arguments. -Require Import Coq.Lists.List +Require Import Stdlib.Lists.List Coq.Program.Program Coq.Arith.Arith - Coq.Strings.String. + Stdlib.Strings.String. Require Import Fiat.ADT Fiat.ADT.ComputationalADT diff --git a/src/Fiat4Monitors/RADLNodeADTs.v b/src/Fiat4Monitors/RADLNodeADTs.v index 101b22f3d..ef707ad61 100644 --- a/src/Fiat4Monitors/RADLNodeADTs.v +++ b/src/Fiat4Monitors/RADLNodeADTs.v @@ -1,9 +1,9 @@ Set Implicit Arguments. -Require Import Coq.Lists.List +Require Import Stdlib.Lists.List Coq.Program.Program Coq.Arith.Arith - Coq.Strings.String. + Stdlib.Strings.String. Require Import Fiat.ADT Fiat.ADT.ComputationalADT diff --git a/src/Fiat4Monitors/RADL_Flag.v b/src/Fiat4Monitors/RADL_Flag.v index 24969c90e..d2f6e7ace 100644 --- a/src/Fiat4Monitors/RADL_Flag.v +++ b/src/Fiat4Monitors/RADL_Flag.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Arith.Arith diff --git a/src/Fiat4Monitors/RADL_Flags.v b/src/Fiat4Monitors/RADL_Flags.v index 3723cd88e..5f5a6695f 100644 --- a/src/Fiat4Monitors/RADL_Flags.v +++ b/src/Fiat4Monitors/RADL_Flags.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Arith.Arith diff --git a/src/Fiat4Monitors/RADL_Messages.v b/src/Fiat4Monitors/RADL_Messages.v index 6ba2f009b..b248da977 100644 --- a/src/Fiat4Monitors/RADL_Messages.v +++ b/src/Fiat4Monitors/RADL_Messages.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Arith.Arith diff --git a/src/Fiat4Monitors/RADL_Nodes.v b/src/Fiat4Monitors/RADL_Nodes.v index 8e5520ba7..4b8cfd8f6 100644 --- a/src/Fiat4Monitors/RADL_Nodes.v +++ b/src/Fiat4Monitors/RADL_Nodes.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Arith.Arith diff --git a/src/Fiat4Monitors/RADL_Notations.v b/src/Fiat4Monitors/RADL_Notations.v index 6b0a7645e..d56e07d1d 100644 --- a/src/Fiat4Monitors/RADL_Notations.v +++ b/src/Fiat4Monitors/RADL_Notations.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Arith.Arith diff --git a/src/Fiat4Monitors/RADL_Topics.v b/src/Fiat4Monitors/RADL_Topics.v index 523faeac4..c6acf3a5a 100644 --- a/src/Fiat4Monitors/RADL_Topics.v +++ b/src/Fiat4Monitors/RADL_Topics.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Arith.Arith diff --git a/src/Fiat4Monitors/TurretMonitor.v b/src/Fiat4Monitors/TurretMonitor.v index 93ebc4c5e..d00ea5fca 100644 --- a/src/Fiat4Monitors/TurretMonitor.v +++ b/src/Fiat4Monitors/TurretMonitor.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Coq.Program.Program Coq.Arith.Arith. +Require Import Stdlib.Lists.List Stdlib.Program.Program Stdlib.Arith.Arith. Require Import Fiat.Fiat4Monitors.RADL_Definitions Fiat.Fiat4Monitors.TurretMonitorSpec Fiat.Fiat4Monitors.MonitorADTs diff --git a/src/Fiat4Monitors/TurretMonitor/FacadeImpl.v b/src/Fiat4Monitors/TurretMonitor/FacadeImpl.v index c01371337..f1936bb7b 100644 --- a/src/Fiat4Monitors/TurretMonitor/FacadeImpl.v +++ b/src/Fiat4Monitors/TurretMonitor/FacadeImpl.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Program.Program diff --git a/src/Fiat4Monitors/TurretMonitor/FiatSpec.v b/src/Fiat4Monitors/TurretMonitor/FiatSpec.v index b09042775..80490007a 100644 --- a/src/Fiat4Monitors/TurretMonitor/FiatSpec.v +++ b/src/Fiat4Monitors/TurretMonitor/FiatSpec.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Program.Program diff --git a/src/Fiat4Monitors/TurretMonitorSpec.v b/src/Fiat4Monitors/TurretMonitorSpec.v index 632d344f4..ebbc7bea5 100644 --- a/src/Fiat4Monitors/TurretMonitorSpec.v +++ b/src/Fiat4Monitors/TurretMonitorSpec.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Program.Program diff --git a/src/FiniteSetADTs/FiniteSetADT.v b/src/FiniteSetADTs/FiniteSetADT.v index 269c0cc70..ad0c7bfc9 100644 --- a/src/FiniteSetADTs/FiniteSetADT.v +++ b/src/FiniteSetADTs/FiniteSetADT.v @@ -1,5 +1,5 @@ (* Definition of the finite set spec *) -Require Import Coq.Sets.Ensembles +Require Import Stdlib.Sets.Ensembles Fiat.ADT.Core Fiat.Common.Ensembles Fiat.ADT.ComputationalADT diff --git a/src/FiniteSetADTs/FiniteSetADTImplementation.v b/src/FiniteSetADTs/FiniteSetADTImplementation.v index 426cf6fe3..0fbc4c128 100644 --- a/src/FiniteSetADTs/FiniteSetADTImplementation.v +++ b/src/FiniteSetADTs/FiniteSetADTImplementation.v @@ -1,6 +1,6 @@ (* Definition of the finite set spec *) Require Export Fiat.FiniteSetADTs.FiniteSetADT. -Require Import Coq.Strings.String Coq.Sets.Ensembles +From Stdlib Require Import String Ensembles Coq.Sets.Finite_sets Coq.Lists.List Coq.Sorting.Permutation Coq.MSets.MSetInterface Coq.MSets.MSetAVL Coq.MSets.MSetList Coq.MSets.MSetRBT diff --git a/src/FiniteSetADTs/FiniteSetADTMethodLaws.v b/src/FiniteSetADTs/FiniteSetADTMethodLaws.v index 612a8984b..68f8f6802 100644 --- a/src/FiniteSetADTs/FiniteSetADTMethodLaws.v +++ b/src/FiniteSetADTs/FiniteSetADTMethodLaws.v @@ -1,5 +1,5 @@ (* Definition of the finite set spec *) -Require Import Coq.Strings.String +From Stdlib Require Import String Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Lists.List diff --git a/src/FiniteSetADTs/FiniteSetRefinement.v b/src/FiniteSetADTs/FiniteSetRefinement.v index 5af4599c7..62f0ce7bc 100644 --- a/src/FiniteSetADTs/FiniteSetRefinement.v +++ b/src/FiniteSetADTs/FiniteSetRefinement.v @@ -1,6 +1,6 @@ (** * Refinement of computations involving ensembles, to ones using finite sets *) -Require Import Coq.Strings.String +From Stdlib Require Import String Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Lists.List diff --git a/src/FiniteSetADTs/WordInterface.v b/src/FiniteSetADTs/WordInterface.v index 88c9ff6a7..2c48c61a6 100644 --- a/src/FiniteSetADTs/WordInterface.v +++ b/src/FiniteSetADTs/WordInterface.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** Before we integrated bedrock, we used a dummy implementation of this module using [nat]; see NatWord.v. *) -Require Import Coq.Classes.Morphisms. +Require Import Stdlib.Classes.Morphisms. Set Implicit Arguments. Global Set Asymmetric Patterns. diff --git a/src/Narcissus/BinLib/AlignedByteBuffer.v b/src/Narcissus/BinLib/AlignedByteBuffer.v index 9db47f81b..c9ffce516 100644 --- a/src/Narcissus/BinLib/AlignedByteBuffer.v +++ b/src/Narcissus/BinLib/AlignedByteBuffer.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. diff --git a/src/Narcissus/BinLib/AlignedByteString.v b/src/Narcissus/BinLib/AlignedByteString.v index dd9526c7d..5a863add6 100644 --- a/src/Narcissus/BinLib/AlignedByteString.v +++ b/src/Narcissus/BinLib/AlignedByteString.v @@ -1388,7 +1388,7 @@ Proof. Qed. Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector. diff --git a/src/Narcissus/BinLib/AlignedDecoders.v b/src/Narcissus/BinLib/AlignedDecoders.v index 085fab0b4..30c116096 100644 --- a/src/Narcissus/BinLib/AlignedDecoders.v +++ b/src/Narcissus/BinLib/AlignedDecoders.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import Coq.ZArith.ZArith - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. diff --git a/src/Narcissus/BinLib/AlignedDomainName.v b/src/Narcissus/BinLib/AlignedDomainName.v index 962a2d267..276bece2c 100644 --- a/src/Narcissus/BinLib/AlignedDomainName.v +++ b/src/Narcissus/BinLib/AlignedDomainName.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import Coq.ZArith.ZArith - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. diff --git a/src/Narcissus/BinLib/AlignedFix.v b/src/Narcissus/BinLib/AlignedFix.v index 891d0e07f..0f4cb1ed4 100644 --- a/src/Narcissus/BinLib/AlignedFix.v +++ b/src/Narcissus/BinLib/AlignedFix.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. diff --git a/src/Narcissus/BinLib/AlignedIPChecksum.v b/src/Narcissus/BinLib/AlignedIPChecksum.v index 8d99ee608..fe4900a49 100644 --- a/src/Narcissus/BinLib/AlignedIPChecksum.v +++ b/src/Narcissus/BinLib/AlignedIPChecksum.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith. diff --git a/src/Narcissus/BinLib/AlignedList.v b/src/Narcissus/BinLib/AlignedList.v index 2226b0a7e..cb2e82c03 100644 --- a/src/Narcissus/BinLib/AlignedList.v +++ b/src/Narcissus/BinLib/AlignedList.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. diff --git a/src/Narcissus/BinLib/AlignedString.v b/src/Narcissus/BinLib/AlignedString.v index 62e2e3f56..1c676bded 100644 --- a/src/Narcissus/BinLib/AlignedString.v +++ b/src/Narcissus/BinLib/AlignedString.v @@ -2,7 +2,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import Coq.ZArith.ZArith Coq.Strings.Ascii - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. diff --git a/src/Narcissus/BinLib/AlignedSumType.v b/src/Narcissus/BinLib/AlignedSumType.v index 4790db70a..ac3547b02 100644 --- a/src/Narcissus/BinLib/AlignedSumType.v +++ b/src/Narcissus/BinLib/AlignedSumType.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. diff --git a/src/Narcissus/Examples/ByteAlignedExample.v b/src/Narcissus/Examples/ByteAlignedExample.v index ca4f48470..c5b9a38aa 100644 --- a/src/Narcissus/Examples/ByteAlignedExample.v +++ b/src/Narcissus/Examples/ByteAlignedExample.v @@ -1,6 +1,6 @@ Require Import Coq.ZArith.ZArith - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector. Require Import diff --git a/src/Narcissus/Examples/DNS/DNSPacket.v b/src/Narcissus/Examples/DNS/DNSPacket.v index da04b2d03..14c986709 100644 --- a/src/Narcissus/Examples/DNS/DNSPacket.v +++ b/src/Narcissus/Examples/DNS/DNSPacket.v @@ -2,7 +2,7 @@ Require Import Coq.Vectors.Vector Coq.ZArith.ZArith Coq.Strings.Ascii - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Vectors.Vector Coq.Lists.List. diff --git a/src/Narcissus/Examples/DNS/DnsOpt.v b/src/Narcissus/Examples/DNS/DnsOpt.v index d299562ed..58e927543 100644 --- a/src/Narcissus/Examples/DNS/DnsOpt.v +++ b/src/Narcissus/Examples/DNS/DnsOpt.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. diff --git a/src/Narcissus/Examples/DNS/RRecordTypes.v b/src/Narcissus/Examples/DNS/RRecordTypes.v index 6445cc362..e675b50b4 100644 --- a/src/Narcissus/Examples/DNS/RRecordTypes.v +++ b/src/Narcissus/Examples/DNS/RRecordTypes.v @@ -2,7 +2,7 @@ Require Import Coq.Vectors.Vector Coq.ZArith.ZArith Coq.Strings.Ascii - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Vectors.Vector Coq.Lists.List. diff --git a/src/Narcissus/Examples/DNS/SimpleDNSPacket.v b/src/Narcissus/Examples/DNS/SimpleDNSPacket.v index 39800c806..d2523ec09 100644 --- a/src/Narcissus/Examples/DNS/SimpleDNSPacket.v +++ b/src/Narcissus/Examples/DNS/SimpleDNSPacket.v @@ -2,7 +2,7 @@ Require Import Coq.Vectors.Vector Coq.ZArith.ZArith Coq.Strings.Ascii - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Vectors.Vector Coq.Lists.List. diff --git a/src/Narcissus/Examples/DNS/SimpleDnsOpt.v b/src/Narcissus/Examples/DNS/SimpleDnsOpt.v index 76289f4cc..e2e40a7e0 100644 --- a/src/Narcissus/Examples/DNS/SimpleDnsOpt.v +++ b/src/Narcissus/Examples/DNS/SimpleDnsOpt.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. @@ -1631,7 +1631,7 @@ Section DnsPacket. End DnsPacket. (*Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. diff --git a/src/Narcissus/Examples/DNS/SimpleRRecordTypes.v b/src/Narcissus/Examples/DNS/SimpleRRecordTypes.v index c5e7ae470..c6c4b8d9c 100644 --- a/src/Narcissus/Examples/DNS/SimpleRRecordTypes.v +++ b/src/Narcissus/Examples/DNS/SimpleRRecordTypes.v @@ -2,7 +2,7 @@ Require Import Coq.Vectors.Vector Coq.ZArith.ZArith Coq.Strings.Ascii - Coq.Strings.String + Stdlib.Strings.String Coq.Bool.Bool Coq.Vectors.Vector Coq.Lists.List. diff --git a/src/Narcissus/Examples/DNS/SimpleResourceRecord.v b/src/Narcissus/Examples/DNS/SimpleResourceRecord.v index 5655bdb14..f72ff39c4 100644 --- a/src/Narcissus/Examples/DNS/SimpleResourceRecord.v +++ b/src/Narcissus/Examples/DNS/SimpleResourceRecord.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. @@ -1640,7 +1640,7 @@ Section DnsPacket. End DnsPacket. (*Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult Coq.Vectors.Vector. diff --git a/src/Narcissus/Examples/Guard/Core.v b/src/Narcissus/Examples/Guard/Core.v index 88944b7a0..3e5080c6a 100644 --- a/src/Narcissus/Examples/Guard/Core.v +++ b/src/Narcissus/Examples/Guard/Core.v @@ -1,5 +1,5 @@ Require Export BinNat. -Require Export Coq.Lists.List. +Require Export Stdlib.Lists.List. Export ListNotations. Require Export Bedrock.Word. diff --git a/src/Narcissus/Examples/Guard/IPTables.v b/src/Narcissus/Examples/Guard/IPTables.v index 9f0c24776..4b3127606 100644 --- a/src/Narcissus/Examples/Guard/IPTables.v +++ b/src/Narcissus/Examples/Guard/IPTables.v @@ -1,6 +1,6 @@ (** This file implements a limited form of iptables syntax. **) -Require Import Coq.Lists.List. +From Stdlib Require Import List. Import ListNotations. Require Import Fiat.Narcissus.Examples.Guard.Core. @@ -209,7 +209,7 @@ Definition cond_dstaddr (spec: address_spec) fun pkt => match_address spec pkt.(ipv4_dest). Arguments cond_dstaddr spec%_addr. -Require Import Coq.Vectors.Vector. +Require Import Stdlib.Vectors.Vector. Import VectorNotations. (* Check if the packet encapsulates a given protocol *) diff --git a/src/Narcissus/Examples/Guard/IPTablesDemos.v b/src/Narcissus/Examples/Guard/IPTablesDemos.v index ca5e9e40b..aa4dc19c7 100644 --- a/src/Narcissus/Examples/Guard/IPTablesDemos.v +++ b/src/Narcissus/Examples/Guard/IPTablesDemos.v @@ -40,7 +40,7 @@ Example drop_dhcp_messages_to_wrong_address := (** We can apply these filters to packets: *) -Require Import Coq.Vectors.Vector. +Require Import Stdlib.Vectors.Vector. Import VectorNotations. Definition dhcp_offer : Vector.t (word 8) _ := Eval compute in Vector.map (@NToWord 8) [69; 0; 1; 72; 4; 69; 0; 0; 128; 17; 180; 4; 192; 168; 0; 1; 192; 168; 0; 10; 0; 67; 0; 68; 1; 52; 34; 51; 2; 1; 6; 0; 0; 0; 61; 29; 0; 0; 0; 0; 0; 0; 0; 0; 192; 168; 0; 10; 192; 168; 0; 1; 0; 0; 0; 0; 0; 11; 130; 1; 252; 66; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 99; 130; 83; 99; 53; 1; 2; 1; 4; 255; 255; 255; 0; 58; 4; 0; 0; 7; 8; 59; 4; 0; 0; 12; 78; 51; 4; 0; 0; 14; 16; 54; 4; 192; 168; 0; 1; 255; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0]%N. diff --git a/src/Narcissus/Examples/Guard/StatefulGuard.v b/src/Narcissus/Examples/Guard/StatefulGuard.v index c40971aaf..a27eb49eb 100644 --- a/src/Narcissus/Examples/Guard/StatefulGuard.v +++ b/src/Narcissus/Examples/Guard/StatefulGuard.v @@ -1,8 +1,8 @@ Require Import Fiat.Narcissus.Examples.NetworkStack.IPv4Header. Require Import Fiat.Narcissus.Examples.NetworkStack.TCP_Packet. Require Import Bedrock.Word. -Require Import Coq.Arith.Arith. -Require Import Coq.Lists.List. +Require Import Stdlib.Arith.Arith. +From Stdlib Require Import List. Require Import Fiat.QueryStructure.Automation.MasterPlan. Require Import Fiat.Common.Ensembles.IndexedEnsembles. Require Import Fiat.Narcissus.Examples.Guard.Core. diff --git a/src/Narcissus/Examples/Guard/StatefulGuardExtraction.v b/src/Narcissus/Examples/Guard/StatefulGuardExtraction.v index 765d6fb7c..9b8e2d0c5 100644 --- a/src/Narcissus/Examples/Guard/StatefulGuardExtraction.v +++ b/src/Narcissus/Examples/Guard/StatefulGuardExtraction.v @@ -29,7 +29,7 @@ Extract Inlined Constant AlignedDecodeMonad.Vector_nth_opt => "ListVector.nth_op Extract Inlined Constant ith => "ListVector.ith". Extract Inlined Constant ith2 => "ListVector.ith2". -Require Import Coq.extraction.ExtrOcamlZInt. +Require Import Stdlib.extraction.ExtrOcamlZInt. Print ADTImplMethods. Print guard_init. diff --git a/src/Narcissus/Examples/ICMP_Packet.v b/src/Narcissus/Examples/ICMP_Packet.v index c44ad0db3..4e8570748 100644 --- a/src/Narcissus/Examples/ICMP_Packet.v +++ b/src/Narcissus/Examples/ICMP_Packet.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector. Require Import diff --git a/src/Narcissus/Examples/NetworkStack/ARPPacket.v b/src/Narcissus/Examples/NetworkStack/ARPPacket.v index d13c8cad4..23299a9db 100644 --- a/src/Narcissus/Examples/NetworkStack/ARPPacket.v +++ b/src/Narcissus/Examples/NetworkStack/ARPPacket.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith. diff --git a/src/Narcissus/Examples/NetworkStack/EthernetHeader.v b/src/Narcissus/Examples/NetworkStack/EthernetHeader.v index a453cfaf7..ec23b421f 100644 --- a/src/Narcissus/Examples/NetworkStack/EthernetHeader.v +++ b/src/Narcissus/Examples/NetworkStack/EthernetHeader.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith. diff --git a/src/Narcissus/Examples/NetworkStack/Fiat4Mirage.v b/src/Narcissus/Examples/NetworkStack/Fiat4Mirage.v index fa8756e19..ac556ff06 100644 --- a/src/Narcissus/Examples/NetworkStack/Fiat4Mirage.v +++ b/src/Narcissus/Examples/NetworkStack/Fiat4Mirage.v @@ -4,7 +4,7 @@ Require Import Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad. -Require Import Coq.Strings.String. +From Stdlib Require Import String. Open Scope string_scope. Require Import Fiat.Common.EnumType. diff --git a/src/Narcissus/Examples/NetworkStack/IPv4Header.v b/src/Narcissus/Examples/NetworkStack/IPv4Header.v index 0dddae9d9..206092568 100644 --- a/src/Narcissus/Examples/NetworkStack/IPv4Header.v +++ b/src/Narcissus/Examples/NetworkStack/IPv4Header.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith. diff --git a/src/Narcissus/Examples/NetworkStack/TCP_Packet.v b/src/Narcissus/Examples/NetworkStack/TCP_Packet.v index f0aaec744..2873ab1d8 100644 --- a/src/Narcissus/Examples/NetworkStack/TCP_Packet.v +++ b/src/Narcissus/Examples/NetworkStack/TCP_Packet.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith. diff --git a/src/Narcissus/Examples/NetworkStack/TestInfrastructure.v b/src/Narcissus/Examples/NetworkStack/TestInfrastructure.v index b6d16b6ce..4306727b5 100644 --- a/src/Narcissus/Examples/NetworkStack/TestInfrastructure.v +++ b/src/Narcissus/Examples/NetworkStack/TestInfrastructure.v @@ -7,8 +7,8 @@ Require Import Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Fiat.Narcissus.Examples.NetworkStack.UDP_Packet. -Require Coq.Vectors.Vector. -Export Coq.Vectors.Vector.VectorNotations. +From Stdlib Require Vector. +Export Stdlib.Vectors.Vector.VectorNotations. (* Require Export *) (* Fiat.Common.SumType *) diff --git a/src/Narcissus/Examples/NetworkStack/UDP_Packet.v b/src/Narcissus/Examples/NetworkStack/UDP_Packet.v index 12086e157..381e15e59 100644 --- a/src/Narcissus/Examples/NetworkStack/UDP_Packet.v +++ b/src/Narcissus/Examples/NetworkStack/UDP_Packet.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith. diff --git a/src/Narcissus/Examples/TutorialPrelude.v b/src/Narcissus/Examples/TutorialPrelude.v index c942ee655..086f47dbf 100644 --- a/src/Narcissus/Examples/TutorialPrelude.v +++ b/src/Narcissus/Examples/TutorialPrelude.v @@ -1,6 +1,6 @@ Require Export Coq.ZArith.ZArith - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector. Require Export Fiat.Computation diff --git a/src/Narcissus/Formats/ASN1.v b/src/Narcissus/Formats/ASN1.v index f968c8f42..749fabcf5 100644 --- a/src/Narcissus/Formats/ASN1.v +++ b/src/Narcissus/Formats/ASN1.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Lists.List. +From Stdlib Require Import List. Inductive ty : Set := | base : ty | arr : list ty -> ty -> ty. @@ -23,7 +23,7 @@ Inductive ty_Prop' : ty -> Prop := Require Import Coq.Strings.Ascii - Coq.Strings.String + Stdlib.Strings.String Coq.Numbers.BinNums Fiat.Common Fiat.Computation.Notations diff --git a/src/Narcissus/Formats/Base/EnqueueFormat.v b/src/Narcissus/Formats/Base/EnqueueFormat.v index d43bf7d31..aadbb1e85 100644 --- a/src/Narcissus/Formats/Base/EnqueueFormat.v +++ b/src/Narcissus/Formats/Base/EnqueueFormat.v @@ -1,6 +1,6 @@ Require Import Coq.ZArith.ZArith - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector. Require Import diff --git a/src/Narcissus/Formats/Base/FMapFormat.v b/src/Narcissus/Formats/Base/FMapFormat.v index c552328ff..7a81e1753 100644 --- a/src/Narcissus/Formats/Base/FMapFormat.v +++ b/src/Narcissus/Formats/Base/FMapFormat.v @@ -1,6 +1,6 @@ Require Import Coq.ZArith.ZArith - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector. Require Import diff --git a/src/Narcissus/Formats/Base/FixFormat.v b/src/Narcissus/Formats/Base/FixFormat.v index 8c87ad0ba..fbfbdeaca 100644 --- a/src/Narcissus/Formats/Base/FixFormat.v +++ b/src/Narcissus/Formats/Base/FixFormat.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import Coq.ZArith.ZArith - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector. Require Import diff --git a/src/Narcissus/Formats/Base/LaxTerminalFormat.v b/src/Narcissus/Formats/Base/LaxTerminalFormat.v index feaaea46a..5f4967237 100644 --- a/src/Narcissus/Formats/Base/LaxTerminalFormat.v +++ b/src/Narcissus/Formats/Base/LaxTerminalFormat.v @@ -1,6 +1,6 @@ Require Import Coq.ZArith.ZArith - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector. Require Import diff --git a/src/Narcissus/Formats/Base/StrictTerminalFormat.v b/src/Narcissus/Formats/Base/StrictTerminalFormat.v index 6e58ade24..064abdd04 100644 --- a/src/Narcissus/Formats/Base/StrictTerminalFormat.v +++ b/src/Narcissus/Formats/Base/StrictTerminalFormat.v @@ -1,6 +1,6 @@ Require Import Coq.ZArith.ZArith - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector. Require Import diff --git a/src/Narcissus/Formats/DomainNameOpt.v b/src/Narcissus/Formats/DomainNameOpt.v index a29bef6de..ff9ded78a 100644 --- a/src/Narcissus/Formats/DomainNameOpt.v +++ b/src/Narcissus/Formats/DomainNameOpt.v @@ -3,7 +3,7 @@ Require Import Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii - Coq.Strings.String + Stdlib.Strings.String Coq.Logic.Eqdep_dec. Require Import diff --git a/src/Narcissus/Formats/FixStringOpt.v b/src/Narcissus/Formats/FixStringOpt.v index 170df43f8..11e79d500 100644 --- a/src/Narcissus/Formats/FixStringOpt.v +++ b/src/Narcissus/Formats/FixStringOpt.v @@ -6,7 +6,7 @@ Require Import Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii - Coq.Strings.String. + Stdlib.Strings.String. Section String. (* this has an exact idential structure to _FixList_ *) diff --git a/src/Narcissus/Formats/IPChecksum.v b/src/Narcissus/Formats/IPChecksum.v index 38bdf8c5a..de8a7a6a9 100644 --- a/src/Narcissus/Formats/IPChecksum.v +++ b/src/Narcissus/Formats/IPChecksum.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import Coq.ZArith.ZArith - Coq.Strings.String + Stdlib.Strings.String Coq.Vectors.Vector. Require Import diff --git a/src/Narcissus/Formats/InternetChecksum.v b/src/Narcissus/Formats/InternetChecksum.v index 9e590dbde..bed2c306e 100644 --- a/src/Narcissus/Formats/InternetChecksum.v +++ b/src/Narcissus/Formats/InternetChecksum.v @@ -318,7 +318,7 @@ Hint Rewrite <- Z.lt_add_lt_sub_l : normalizeZ. Hint Rewrite <- Z.lt_add_lt_sub_r : normalizeZ. Hint Rewrite @gt_minus_one_ge_zero : normalizeZ. -Require Import Coq.micromega.Psatz. +Require Import Stdlib.micromega.Psatz. Notation OneC_InRange p z := ((- Z.of_N (Npow2 p)) < z < Z.of_N (Npow2 p)). diff --git a/src/Narcissus/Formats/StringOpt.v b/src/Narcissus/Formats/StringOpt.v index eada34e8d..f73c0af60 100644 --- a/src/Narcissus/Formats/StringOpt.v +++ b/src/Narcissus/Formats/StringOpt.v @@ -4,7 +4,7 @@ Require Import Require Import Bedrock.Word Coq.Strings.Ascii - Coq.Strings.String. + Stdlib.Strings.String. Section String. (* this has an exact idential structure to _FixList_ *) diff --git a/src/Narcissus/OCamlExtraction/Extraction.v b/src/Narcissus/OCamlExtraction/Extraction.v index 2acf6c07a..44113fca9 100644 --- a/src/Narcissus/OCamlExtraction/Extraction.v +++ b/src/Narcissus/OCamlExtraction/Extraction.v @@ -17,12 +17,12 @@ if x <= y then 0 else (x - y)". (** A few additional tweaks *) Require Import Fiat.Common.String_as_OT. -Require Import Coq.Structures.OrderedTypeEx. +Require Import Stdlib.Structures.OrderedTypeEx. Extraction Inline negb. Extract Inductive Bool.reflect => bool [ true false ]. -Extract Constant Coq.Strings.String.string_dec => "(=)". +Extract Constant Stdlib.Strings.String.string_dec => "(=)". Extract Constant String_as_OT.eq_dec => "(=)". Extract Constant Nat_as_OT.eq_dec => "(=)". diff --git a/src/Narcissus/Stores/Cache.v b/src/Narcissus/Stores/Cache.v index 289c6f16f..7caca5878 100644 --- a/src/Narcissus/Stores/Cache.v +++ b/src/Narcissus/Stores/Cache.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List +Require Import Stdlib.Lists.List Fiat.Computation. Set Implicit Arguments. diff --git a/src/Narcissus/Stores/DomainNameStore.v b/src/Narcissus/Stores/DomainNameStore.v index 6fac1d515..ce00e5cca 100644 --- a/src/Narcissus/Stores/DomainNameStore.v +++ b/src/Narcissus/Stores/DomainNameStore.v @@ -2,7 +2,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. Require Import Coq.ZArith.ZArith Coq.Lists.List - Coq.Strings.String + Stdlib.Strings.String Coq.Arith.Mult. Require Import diff --git a/src/Parsers/AbstractInterpretation/NonTerminalMap.v b/src/Parsers/AbstractInterpretation/NonTerminalMap.v index 5887df386..50525b0c6 100644 --- a/src/Parsers/AbstractInterpretation/NonTerminalMap.v +++ b/src/Parsers/AbstractInterpretation/NonTerminalMap.v @@ -1,7 +1,7 @@ -Require Import Coq.PArith.BinPos Coq.PArith.Pnat. -Require Import Coq.Arith.Arith. -Require Import Coq.FSets.FMapInterface. -Require Import Coq.FSets.FMapPositive. +Require Import Stdlib.PArith.BinPos Stdlib.PArith.Pnat. +Require Import Stdlib.Arith.Arith. +Require Import Stdlib.FSets.FMapInterface. +Require Import Stdlib.FSets.FMapPositive. Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Common.List.ListFacts. Require Import Fiat.Common.List.ListMorphisms. diff --git a/src/Parsers/BaseTypes.v b/src/Parsers/BaseTypes.v index d749e9f78..5a851f508 100644 --- a/src/Parsers/BaseTypes.v +++ b/src/Parsers/BaseTypes.v @@ -1,5 +1,5 @@ (** * Definition of the common part of the interface of the CFG parser *) -Require Import Coq.Lists.List Coq.Arith.Wf_nat. +From Stdlib Require Import List Wf_nat. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Set Implicit Arguments. diff --git a/src/Parsers/BaseTypesLemmas.v b/src/Parsers/BaseTypesLemmas.v index 340a95630..5785908c2 100644 --- a/src/Parsers/BaseTypesLemmas.v +++ b/src/Parsers/BaseTypesLemmas.v @@ -1,7 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Lemmas about the common part of the interface of the CFG parser *) -Require Import Coq.Classes.RelationClasses Coq.Setoids.Setoid. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import RelationClasses Setoid ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. diff --git a/src/Parsers/BooleanRecognizerCorrect.v b/src/Parsers/BooleanRecognizerCorrect.v index ce1dd16b0..c9add332a 100644 --- a/src/Parsers/BooleanRecognizerCorrect.v +++ b/src/Parsers/BooleanRecognizerCorrect.v @@ -1,4 +1,4 @@ -Require Import Coq.Classes.Morphisms. +Require Import Stdlib.Classes.Morphisms. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes Fiat.Parsers.CorrectnessBaseTypes. Require Import Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericCorrectnessBaseTypes. diff --git a/src/Parsers/BooleanRecognizerExt.v b/src/Parsers/BooleanRecognizerExt.v index cfb231438..df732d528 100644 --- a/src/Parsers/BooleanRecognizerExt.v +++ b/src/Parsers/BooleanRecognizerExt.v @@ -1,5 +1,5 @@ (** * Extensionality of boolean recognizer *) -Require Import Coq.Classes.Morphisms. +Require Import Stdlib.Classes.Morphisms. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Parsers.BooleanRecognizer. diff --git a/src/Parsers/BooleanRecognizerOptimized.v b/src/Parsers/BooleanRecognizerOptimized.v index c22d1c655..68f0673d5 100644 --- a/src/Parsers/BooleanRecognizerOptimized.v +++ b/src/Parsers/BooleanRecognizerOptimized.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Definition of a boolean-returning CFG parser-recognizer *) -Require Import Coq.Lists.List Coq.Strings.String. -Require Import Coq.Arith.Compare_dec Coq.Arith.Wf_nat Coq.Arith.PeanoNat. +Require Import Stdlib.Lists.List Stdlib.Strings.String. +Require Import Stdlib.Arith.Compare_dec Stdlib.Arith.Wf_nat Stdlib.Arith.PeanoNat. Require Import Fiat.Common.List.Operations. Require Import Fiat.Common.List.ListMorphisms. Require Import Fiat.Parsers.ContextFreeGrammar.Core. diff --git a/src/Parsers/BooleanRecognizerTests.v b/src/Parsers/BooleanRecognizerTests.v index db21575e7..a713a8bed 100644 --- a/src/Parsers/BooleanRecognizerTests.v +++ b/src/Parsers/BooleanRecognizerTests.v @@ -1,6 +1,6 @@ (** * Some simple examples with the boolean-returning CFG parser-recognizer *) -Require Import Coq.Lists.List Coq.Strings.String. -Require Import Coq.Arith.PeanoNat Coq.Arith.Compare_dec Coq.Arith.Wf_nat. +Require Import Stdlib.Lists.List Stdlib.Strings.String. +Require Import Stdlib.Arith.PeanoNat Stdlib.Arith.Compare_dec Stdlib.Arith.Wf_nat. Require Import Fiat.Parsers.Grammars.Trivial Fiat.Parsers.Grammars.ABStar. Require Import Fiat.Parsers.Splitters.RDPList Fiat.Parsers.Splitters.BruteForce. Require Import Fiat.Parsers.ContextFreeGrammar.Core. diff --git a/src/Parsers/ContextFreeGrammar/Carriers.v b/src/Parsers/ContextFreeGrammar/Carriers.v index f73bbb4f5..fa8e4b48d 100644 --- a/src/Parsers/ContextFreeGrammar/Carriers.v +++ b/src/Parsers/ContextFreeGrammar/Carriers.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Common.Enumerable. Require Import Fiat.Common.Enumerable.BoolProp. Require Import Fiat.Common.List.Operations. diff --git a/src/Parsers/ContextFreeGrammar/Core.v b/src/Parsers/ContextFreeGrammar/Core.v index 6457bc344..3461f8c0f 100644 --- a/src/Parsers/ContextFreeGrammar/Core.v +++ b/src/Parsers/ContextFreeGrammar/Core.v @@ -1,5 +1,5 @@ (** * Definition of Context Free Grammars *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Export Fiat.Parsers.StringLike.Core. Import ListNotations. diff --git a/src/Parsers/ContextFreeGrammar/ExplorationUtil.v b/src/Parsers/ContextFreeGrammar/ExplorationUtil.v index 5bf4a90af..7ac205549 100644 --- a/src/Parsers/ContextFreeGrammar/ExplorationUtil.v +++ b/src/Parsers/ContextFreeGrammar/ExplorationUtil.v @@ -1,11 +1,11 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.micromega.Lia. -Require Import Coq.PArith.BinPos. -Require Import Coq.Lists.List. -Require Import Coq.Sorting.Mergesort. -Require Import Coq.Structures.OrdersEx. -Require Import Coq.Strings.Ascii. -Require Import Coq.Strings.String. +Require Import Stdlib.micromega.Lia. +Require Import Stdlib.PArith.BinPos. +From Stdlib Require Import List. +Require Import Stdlib.Sorting.Mergesort. +Require Import Stdlib.Structures.OrdersEx. +Require Import Stdlib.Strings.Ascii. +From Stdlib Require Import String. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Parsers.ContextFreeGrammar.Reflective. diff --git a/src/Parsers/ContextFreeGrammar/Fix/AsciiLattice.v b/src/Parsers/ContextFreeGrammar/Fix/AsciiLattice.v index 0a84bf66e..ec815f95d 100644 --- a/src/Parsers/ContextFreeGrammar/Fix/AsciiLattice.v +++ b/src/Parsers/ContextFreeGrammar/Fix/AsciiLattice.v @@ -1,5 +1,5 @@ -Require Import Coq.Strings.Ascii. -Require Import Coq.MSets.MSetPositive. +Require Import Stdlib.Strings.Ascii. +Require Import Stdlib.MSets.MSetPositive. Require Import Fiat.Parsers.ContextFreeGrammar.Fix.Definitions. Require Import Fiat.Common.MSetBoundedLattice. Require Import Fiat.Common.MSetExtensions. diff --git a/src/Parsers/ContextFreeGrammar/Fix/Definitions.v b/src/Parsers/ContextFreeGrammar/Fix/Definitions.v index eef0c1f71..6a1dec50a 100644 --- a/src/Parsers/ContextFreeGrammar/Fix/Definitions.v +++ b/src/Parsers/ContextFreeGrammar/Fix/Definitions.v @@ -1,6 +1,6 @@ -Require Import Coq.PArith.BinPos Coq.PArith.Pnat. -Require Import Coq.Arith.Arith. -Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms. +Require Import Stdlib.PArith.BinPos Stdlib.PArith.Pnat. +Require Import Stdlib.Arith.Arith. +Require Import Stdlib.Classes.RelationClasses Stdlib.Classes.Morphisms. Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Common.Tactics.SplitInContext. Require Import Fiat.Common.Notations. diff --git a/src/Parsers/ContextFreeGrammar/Fix/Fix.v b/src/Parsers/ContextFreeGrammar/Fix/Fix.v index 08296970e..5be8c8866 100644 --- a/src/Parsers/ContextFreeGrammar/Fix/Fix.v +++ b/src/Parsers/ContextFreeGrammar/Fix/Fix.v @@ -1,6 +1,6 @@ -Require Import Coq.Init.Wf Coq.Numbers.BinNums. -Require Import Coq.Arith.Arith. -Require Import Coq.FSets.FMapPositive. +Require Import Stdlib.Init.Wf Stdlib.Numbers.BinNums. +Require Import Stdlib.Arith.Arith. +Require Import Stdlib.FSets.FMapPositive. Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.Splitters.RDPList. diff --git a/src/Parsers/ContextFreeGrammar/Fix/FixRelated.v b/src/Parsers/ContextFreeGrammar/Fix/FixRelated.v index a069b534a..26070d832 100644 --- a/src/Parsers/ContextFreeGrammar/Fix/FixRelated.v +++ b/src/Parsers/ContextFreeGrammar/Fix/FixRelated.v @@ -1,6 +1,6 @@ -Require Import Coq.Init.Wf Coq.Numbers.BinNums. -Require Import Coq.Arith.Arith. -Require Import Coq.FSets.FMapPositive. +Require Import Stdlib.Init.Wf Stdlib.Numbers.BinNums. +Require Import Stdlib.Arith.Arith. +Require Import Stdlib.FSets.FMapPositive. Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.Splitters.RDPList. diff --git a/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretation.v b/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretation.v index 57e57615f..a1ebc039a 100644 --- a/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretation.v +++ b/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretation.v @@ -1,4 +1,4 @@ -Require Import Coq.Sets.Ensembles. +From Stdlib Require Import Ensembles. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Parsers.ContextFreeGrammar.Core. diff --git a/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitions.v b/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitions.v index 11f63726d..a96b5dc4e 100644 --- a/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitions.v +++ b/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitions.v @@ -1,5 +1,5 @@ -Require Import Coq.Sets.Ensembles. -Require Import Coq.Classes.Morphisms. +From Stdlib Require Import Ensembles. +Require Import Stdlib.Classes.Morphisms. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Parsers.ContextFreeGrammar.Core. diff --git a/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitionsRelations.v b/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitionsRelations.v index 80040ad42..6302b15c5 100644 --- a/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitionsRelations.v +++ b/src/Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitionsRelations.v @@ -1,5 +1,5 @@ -Require Import Coq.Sets.Ensembles. -Require Import Coq.Classes.Morphisms. +From Stdlib Require Import Ensembles. +Require Import Stdlib.Classes.Morphisms. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Parsers.ContextFreeGrammar.Core. diff --git a/src/Parsers/ContextFreeGrammar/Fix/ProdAbstractInterpretationDefinitions.v b/src/Parsers/ContextFreeGrammar/Fix/ProdAbstractInterpretationDefinitions.v index a2fcff4fc..f732149ee 100644 --- a/src/Parsers/ContextFreeGrammar/Fix/ProdAbstractInterpretationDefinitions.v +++ b/src/Parsers/ContextFreeGrammar/Fix/ProdAbstractInterpretationDefinitions.v @@ -1,4 +1,4 @@ -Require Import Coq.Sets.Ensembles. +From Stdlib Require Import Ensembles. Require Import Fiat.Parsers.StringLike.Core. Require Import Fiat.Parsers.StringLike.Properties. Require Import Fiat.Parsers.ContextFreeGrammar.Fix.Properties. diff --git a/src/Parsers/ContextFreeGrammar/Fold.v b/src/Parsers/ContextFreeGrammar/Fold.v index 1d9824dfe..99adead01 100644 --- a/src/Parsers/ContextFreeGrammar/Fold.v +++ b/src/Parsers/ContextFreeGrammar/Fold.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * A general [fold] over grammars *) -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import List. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.ContextFreeGrammar.Core. diff --git a/src/Parsers/ContextFreeGrammar/Notations.v b/src/Parsers/ContextFreeGrammar/Notations.v index b2d496264..d6c2606f4 100644 --- a/src/Parsers/ContextFreeGrammar/Notations.v +++ b/src/Parsers/ContextFreeGrammar/Notations.v @@ -1,13 +1,13 @@ (** * Convenience Notations for Describing Context Free Grammars *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Export Fiat.Parsers.ContextFreeGrammar.Reflective. Require Export Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Common.Notations. -Export Coq.NArith.BinNatDef. -Export Coq.Strings.Ascii. -Export Coq.Strings.String. +Export Stdlib.NArith.BinNatDef. +Export Stdlib.Strings.Ascii. +Export Stdlib.Strings.String. Export Fiat.Parsers.ContextFreeGrammar.Core. (** ** Generic setup *) diff --git a/src/Parsers/ContextFreeGrammar/PreNotations.v b/src/Parsers/ContextFreeGrammar/PreNotations.v index dc1a04556..8a56148d2 100644 --- a/src/Parsers/ContextFreeGrammar/PreNotations.v +++ b/src/Parsers/ContextFreeGrammar/PreNotations.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Reflective. Require Import Fiat.Common.List.Operations. diff --git a/src/Parsers/ContextFreeGrammar/PreNotationsLemmas.v b/src/Parsers/ContextFreeGrammar/PreNotationsLemmas.v index d608d2b5a..bd92f0504 100644 --- a/src/Parsers/ContextFreeGrammar/PreNotationsLemmas.v +++ b/src/Parsers/ContextFreeGrammar/PreNotationsLemmas.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String. +From Stdlib Require Import String. Require Import Fiat.Parsers.GenericBaseTypes. Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. diff --git a/src/Parsers/ContextFreeGrammar/Precompute.v b/src/Parsers/ContextFreeGrammar/Precompute.v index 77110d57f..cb91d35cd 100644 --- a/src/Parsers/ContextFreeGrammar/Precompute.v +++ b/src/Parsers/ContextFreeGrammar/Precompute.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String. +From Stdlib Require Import String. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. diff --git a/src/Parsers/ContextFreeGrammar/Properties.v b/src/Parsers/ContextFreeGrammar/Properties.v index e28fe2688..59c8abdc5 100644 --- a/src/Parsers/ContextFreeGrammar/Properties.v +++ b/src/Parsers/ContextFreeGrammar/Properties.v @@ -1,5 +1,5 @@ (** * Properties about Context Free Grammars *) -Require Import Coq.Lists.List Coq.Arith.PeanoNat. +From Stdlib Require Import List PeanoNat. Require Import Fiat.Common Fiat.Common.UIP. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Equality. diff --git a/src/Parsers/ContextFreeGrammar/Reflective.v b/src/Parsers/ContextFreeGrammar/Reflective.v index e7ba65518..3fd857a39 100644 --- a/src/Parsers/ContextFreeGrammar/Reflective.v +++ b/src/Parsers/ContextFreeGrammar/Reflective.v @@ -1,5 +1,5 @@ (** * Reflective notations for context free grammars *) -Require Import Coq.Strings.Ascii. +From Stdlib Require Import Ascii. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Common.Equality. diff --git a/src/Parsers/ContextFreeGrammar/ReflectiveLemmas.v b/src/Parsers/ContextFreeGrammar/ReflectiveLemmas.v index 10db4c96a..bf4e53033 100644 --- a/src/Parsers/ContextFreeGrammar/ReflectiveLemmas.v +++ b/src/Parsers/ContextFreeGrammar/ReflectiveLemmas.v @@ -1,5 +1,5 @@ (** * Leamms for reflective notations for context free grammars *) -Require Import Coq.Strings.Ascii Coq.Classes.Morphisms Coq.Relations.Relation_Definitions. +Require Import Stdlib.Strings.Ascii Stdlib.Classes.Morphisms Stdlib.Relations.Relation_Definitions. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Reflective. diff --git a/src/Parsers/ContextFreeGrammar/SimpleCorrectness.v b/src/Parsers/ContextFreeGrammar/SimpleCorrectness.v index bd86b0398..289b8e777 100644 --- a/src/Parsers/ContextFreeGrammar/SimpleCorrectness.v +++ b/src/Parsers/ContextFreeGrammar/SimpleCorrectness.v @@ -1,5 +1,5 @@ (** * Specification of what it means for a simple_parse_of to be correct *) -Require Import Coq.Lists.List. +From Stdlib Require Import List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. (** We currently have two versions, one defined by [Fixpoint], and another as an inductive. I suspect the fixpoint will be easier to reason with, but I leave both in for now in case this is not the case. *) diff --git a/src/Parsers/ContextFreeGrammar/ValidProperties.v b/src/Parsers/ContextFreeGrammar/ValidProperties.v index c69b15bbf..b2a038cb3 100644 --- a/src/Parsers/ContextFreeGrammar/ValidProperties.v +++ b/src/Parsers/ContextFreeGrammar/ValidProperties.v @@ -1,5 +1,5 @@ (** * Definition of Context Free Grammars *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Export Fiat.Parsers.StringLike.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Equality. diff --git a/src/Parsers/ContextFreeGrammar/ValidReflective.v b/src/Parsers/ContextFreeGrammar/ValidReflective.v index 0c2dec518..1671652f6 100644 --- a/src/Parsers/ContextFreeGrammar/ValidReflective.v +++ b/src/Parsers/ContextFreeGrammar/ValidReflective.v @@ -1,6 +1,6 @@ (** * Definition of Context Free Grammars *) -Require Import Coq.Strings.String Coq.Lists.List. -Require Import Coq.Arith.PeanoNat. +From Stdlib Require Import String List. +Require Import Stdlib.Arith.PeanoNat. Require Export Fiat.Parsers.StringLike.Core. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Parsers.Splitters.RDPList. diff --git a/src/Parsers/CorrectnessBaseTypes.v b/src/Parsers/CorrectnessBaseTypes.v index a0054cebb..12b4df58a 100644 --- a/src/Parsers/CorrectnessBaseTypes.v +++ b/src/Parsers/CorrectnessBaseTypes.v @@ -1,5 +1,5 @@ (** * Definition of a boolean-returning CFG parser-recognizer *) -Require Import Coq.Lists.List. +From Stdlib Require Import List. Require Import Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.MinimalParse. Require Import Fiat.Common. diff --git a/src/Parsers/ExtrOcamlParsers.v b/src/Parsers/ExtrOcamlParsers.v index d74f9ee2b..0dfd4f9e0 100644 --- a/src/Parsers/ExtrOcamlParsers.v +++ b/src/Parsers/ExtrOcamlParsers.v @@ -1,16 +1,16 @@ Require Import Fiat.Common.Equality Fiat.Parsers.ParserFromParserADT. -Require Import Coq.ZArith.BinInt. +Require Import Stdlib.ZArith.BinInt. Require Export Fiat.Parsers.Refinement.Tactics. Require Export Fiat.Common.BoolFacts. Require Export Fiat.ADTNotation.BuildComputationalADT. Require Export Fiat.Common.NatFacts. Require Export Fiat.Parsers.StringLike.FirstCharSuchThat. -Require Export Coq.Strings.Ascii. -Require Export Coq.extraction.ExtrOcamlBasic. -Require Export Coq.extraction.ExtrOcamlNatInt. -Require Export Coq.extraction.ExtrOcamlZInt. -Require Export Coq.extraction.ExtrOcamlString. -Require Export Coq.extraction.ExtrOcamlIntConv. +Require Export Stdlib.Strings.Ascii. +Require Export Stdlib.extraction.ExtrOcamlBasic. +Require Export Stdlib.extraction.ExtrOcamlNatInt. +Require Export Stdlib.extraction.ExtrOcamlZInt. +Require Export Stdlib.extraction.ExtrOcamlString. +Require Export Stdlib.extraction.ExtrOcamlIntConv. Require Export Fiat.Parsers.ExtrOcamlPrimitives. Import ExtrOcamlPrimitives.Ocaml. @@ -185,5 +185,5 @@ Definition line : string := Ocaml.explode line_ocaml. Definition premain_ocaml (parse : Ocaml.string -> bool) : unit := premain' line_ocaml 10 10 parse. -Definition premain (parse : Coq.Strings.String.string -> bool) : unit +Definition premain (parse : Stdlib.Strings.String.string -> bool) : unit := premain' line 10 10 parse. diff --git a/src/Parsers/ExtrOcamlPrimitives.v b/src/Parsers/ExtrOcamlPrimitives.v index d48910ef2..31beb7ef5 100644 --- a/src/Parsers/ExtrOcamlPrimitives.v +++ b/src/Parsers/ExtrOcamlPrimitives.v @@ -1,8 +1,8 @@ -Require Export Coq.extraction.ExtrOcamlIntConv. +Require Export Stdlib.extraction.ExtrOcamlIntConv. -Require Import Coq.ZArith.BinInt. +Require Import Stdlib.ZArith.BinInt. -Require Import Coq.Strings.String. +From Stdlib Require Import String. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Module Import Ocaml. @@ -141,10 +141,10 @@ Module Export OcamlProperties. Module Import StringProperties. Axiom explode_implode : forall s, Ocaml.explode (Ocaml.implode s) = s. Axiom implode_explode : forall s, Ocaml.implode (Ocaml.explode s) = s. - Axiom length_correct : forall s, String.length s = Coq.Strings.String.length (Ocaml.explode s). - Axiom get_correct : forall s n ch, (String.get s n = ch) <-> (Coq.Strings.String.get n (Ocaml.explode s) = Some ch). - Axiom safe_get_correct : forall s n, String.safe_get s n = Coq.Strings.String.get n (Ocaml.explode s). - Axiom sub_correct : forall s start len, String.sub s start len = Ocaml.implode (Coq.Strings.String.substring start len (Ocaml.explode s)). + Axiom length_correct : forall s, String.length s = Stdlib.Strings.String.length (Ocaml.explode s). + Axiom get_correct : forall s n ch, (String.get s n = ch) <-> (Stdlib.Strings.String.get n (Ocaml.explode s) = Some ch). + Axiom safe_get_correct : forall s n, String.safe_get s n = Stdlib.Strings.String.get n (Ocaml.explode s). + Axiom sub_correct : forall s start len, String.sub s start len = Ocaml.implode (Stdlib.Strings.String.substring start len (Ocaml.explode s)). Axiom compare_eq : forall s s', (z_of_int (String.compare s s') = 0%Z) <-> s = s'. Definition compare_eq' s s' (H : s = s') : z_of_int (String.compare s s') = 0%Z diff --git a/src/Parsers/GenericBaseTypes.v b/src/Parsers/GenericBaseTypes.v index 7b026d950..fe2275c9f 100644 --- a/src/Parsers/GenericBaseTypes.v +++ b/src/Parsers/GenericBaseTypes.v @@ -1,5 +1,5 @@ (** * Definition of the generic part of the interface of the CFG parser *) -Require Import Coq.Strings.String. +From Stdlib Require Import String. Require Export Fiat.Common.Coq__8_4__8_5__Compat. Set Implicit Arguments. diff --git a/src/Parsers/GenericCorrectnessBaseTypes.v b/src/Parsers/GenericCorrectnessBaseTypes.v index 59a7eb459..53802d6cc 100644 --- a/src/Parsers/GenericCorrectnessBaseTypes.v +++ b/src/Parsers/GenericCorrectnessBaseTypes.v @@ -1,6 +1,5 @@ (** * Definition of the generic part of the interface of the correctness proof of the CFG parser *) -Require Import Coq.Classes.Morphisms. -Require Import Coq.Arith.EqNat. +From Stdlib Require Import Morphisms EqNat. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.GenericBaseTypes. Require Import Fiat.Parsers.BaseTypes. diff --git a/src/Parsers/GenericRecognizer.v b/src/Parsers/GenericRecognizer.v index c346bd20e..c9714fa5e 100644 --- a/src/Parsers/GenericRecognizer.v +++ b/src/Parsers/GenericRecognizer.v @@ -1,7 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Definition of a CFG parser-recognizer *) -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import List ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Parsers.GenericBaseTypes. diff --git a/src/Parsers/GenericRecognizerMin.v b/src/Parsers/GenericRecognizerMin.v index ee4ac2d07..59561ec51 100644 --- a/src/Parsers/GenericRecognizerMin.v +++ b/src/Parsers/GenericRecognizerMin.v @@ -1,9 +1,9 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Definition of a parse-tree-returning CFG parser-recognizer *) -Require Import Coq.Lists.List. -Require Import Coq.Arith.EqNat. -Require Import Coq.Arith.Compare_dec Coq.Arith.Wf_nat. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import List. +Require Import Stdlib.Arith.EqNat. +Require Import Stdlib.Arith.Compare_dec Stdlib.Arith.Wf_nat. +From Stdlib Require Import ZArith. Require Import Fiat.Common.List.Operations. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. diff --git a/src/Parsers/GenericRecognizerOptimized.v b/src/Parsers/GenericRecognizerOptimized.v index c483af3c3..329d623ef 100644 --- a/src/Parsers/GenericRecognizerOptimized.v +++ b/src/Parsers/GenericRecognizerOptimized.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Definition of an optimized CFG parser-recognizer *) -Require Import Coq.Lists.List Coq.Strings.String. -Require Import Coq.Arith.PeanoNat Coq.Arith.Compare_dec Coq.Arith.Wf_nat. +Require Import Stdlib.Lists.List Stdlib.Strings.String. +Require Import Stdlib.Arith.PeanoNat Stdlib.Arith.Compare_dec Stdlib.Arith.Wf_nat. Require Import Fiat.Common.List.Operations. Require Import Fiat.Common.List.ListMorphisms. Require Import Fiat.Parsers.ContextFreeGrammar.Core. diff --git a/src/Parsers/GenericRecognizerOptimizedTactics.v b/src/Parsers/GenericRecognizerOptimizedTactics.v index 475c51791..d81fefa89 100644 --- a/src/Parsers/GenericRecognizerOptimizedTactics.v +++ b/src/Parsers/GenericRecognizerOptimizedTactics.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Lists.List. -Require Import Coq.Arith.Compare_dec. -Require Import Coq.Arith.PeanoNat. +From Stdlib Require Import List. +Require Import Stdlib.Arith.Compare_dec. +Require Import Stdlib.Arith.PeanoNat. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Parsers.BaseTypesLemmas. Require Import Fiat.Parsers.GenericBaseTypes. diff --git a/src/Parsers/Grammars/EvalGrammarTactics.v b/src/Parsers/Grammars/EvalGrammarTactics.v index 5d8333244..c75e5b9f8 100644 --- a/src/Parsers/Grammars/EvalGrammarTactics.v +++ b/src/Parsers/Grammars/EvalGrammarTactics.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List. -Require Import Coq.Strings.String. +From Stdlib Require Import List. +From Stdlib Require Import String. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. diff --git a/src/Parsers/Grammars/JSONTests.v b/src/Parsers/Grammars/JSONTests.v index fd282e3e6..f7fbf7422 100644 --- a/src/Parsers/Grammars/JSONTests.v +++ b/src/Parsers/Grammars/JSONTests.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Notations. Require Import Fiat.Parsers.StringLike.String. diff --git a/src/Parsers/Grammars/Tests.v b/src/Parsers/Grammars/Tests.v index 404ebdaac..9b6334956 100644 --- a/src/Parsers/Grammars/Tests.v +++ b/src/Parsers/Grammars/Tests.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.Strings.Ascii Coq.Lists.List. +From Stdlib Require Import String Ascii List. Require Import Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Notations. Require Import Fiat.Parsers.StringLike.String. diff --git a/src/Parsers/Grammars/Trivial.v b/src/Parsers/Grammars/Trivial.v index 654686071..dc8873d89 100644 --- a/src/Parsers/Grammars/Trivial.v +++ b/src/Parsers/Grammars/Trivial.v @@ -1,5 +1,5 @@ (** * Definition of ε, the CFG accepting only "" *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. diff --git a/src/Parsers/MinimalParse.v b/src/Parsers/MinimalParse.v index e4c11612e..974fcdb74 100644 --- a/src/Parsers/MinimalParse.v +++ b/src/Parsers/MinimalParse.v @@ -1,5 +1,5 @@ (** * Definition of minimal parse trees *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. diff --git a/src/Parsers/MinimalParseOfParse.v b/src/Parsers/MinimalParseOfParse.v index 54b7733f2..5a2ee8456 100644 --- a/src/Parsers/MinimalParseOfParse.v +++ b/src/Parsers/MinimalParseOfParse.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Every parse tree has a corresponding minimal parse tree *) -Require Import Coq.Strings.String Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import String List. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.WellFoundedParse. Require Import Fiat.Parsers.CorrectnessBaseTypes Fiat.Parsers.BaseTypes. Require Import Fiat.Parsers.StringLike.Properties. diff --git a/src/Parsers/ParserFromParserADT.v b/src/Parsers/ParserFromParserADT.v index f2177e109..4785056b7 100644 --- a/src/Parsers/ParserFromParserADT.v +++ b/src/Parsers/ParserFromParserADT.v @@ -1,5 +1,5 @@ (** Reference implementation of a splitter and parser based on that splitter *) -Require Import Coq.Strings.String. +From Stdlib Require Import String. Require Import Fiat.Common.BoundedLookup. Require Import Fiat.ADT.ComputationalADT. Require Import Fiat.ADTRefinement.GeneralRefinements. diff --git a/src/Parsers/ParserImplementation.v b/src/Parsers/ParserImplementation.v index da6259600..c9b012d71 100644 --- a/src/Parsers/ParserImplementation.v +++ b/src/Parsers/ParserImplementation.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Implementation of simply-typed interface of the parser *) -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Export Fiat.Parsers.ParserInterface. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Properties. diff --git a/src/Parsers/Reachable/All/MinimalReachable.v b/src/Parsers/Reachable/All/MinimalReachable.v index ef7523d58..e4b092c3e 100644 --- a/src/Parsers/Reachable/All/MinimalReachable.v +++ b/src/Parsers/Reachable/All/MinimalReachable.v @@ -1,5 +1,5 @@ (** * Definition of minimal parse trees *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. diff --git a/src/Parsers/Reachable/All/MinimalReachableOfReachable.v b/src/Parsers/Reachable/All/MinimalReachableOfReachable.v index 0aa10217c..e16708ead 100644 --- a/src/Parsers/Reachable/All/MinimalReachableOfReachable.v +++ b/src/Parsers/Reachable/All/MinimalReachableOfReachable.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Every parse tree has a corresponding minimal parse tree *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import String. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.Reachable.All.Reachable. Require Import Fiat.Parsers.Reachable.All.MinimalReachable. diff --git a/src/Parsers/Reachable/All/Reachable.v b/src/Parsers/Reachable/All/Reachable.v index 34dc8ed45..f0be84566 100644 --- a/src/Parsers/Reachable/All/Reachable.v +++ b/src/Parsers/Reachable/All/Reachable.v @@ -1,5 +1,5 @@ (** * Definition of Context Free Grammars *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Common. diff --git a/src/Parsers/Reachable/MaybeEmpty/Core.v b/src/Parsers/Reachable/MaybeEmpty/Core.v index 90ff3c089..683b6f34e 100644 --- a/src/Parsers/Reachable/MaybeEmpty/Core.v +++ b/src/Parsers/Reachable/MaybeEmpty/Core.v @@ -1,5 +1,5 @@ (** * Definition of Context Free Grammars *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Common. diff --git a/src/Parsers/Reachable/MaybeEmpty/Minimal.v b/src/Parsers/Reachable/MaybeEmpty/Minimal.v index 2f1fa0531..61cedadbb 100644 --- a/src/Parsers/Reachable/MaybeEmpty/Minimal.v +++ b/src/Parsers/Reachable/MaybeEmpty/Minimal.v @@ -1,5 +1,5 @@ (** * Definition of minimal parse trees *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. diff --git a/src/Parsers/Reachable/MaybeEmpty/MinimalOfCore.v b/src/Parsers/Reachable/MaybeEmpty/MinimalOfCore.v index bb40bee5c..3570d7961 100644 --- a/src/Parsers/Reachable/MaybeEmpty/MinimalOfCore.v +++ b/src/Parsers/Reachable/MaybeEmpty/MinimalOfCore.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Every parse tree has a corresponding minimal parse tree *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import String. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.Reachable.MaybeEmpty.Core. Require Import Fiat.Parsers.Reachable.MaybeEmpty.Minimal. diff --git a/src/Parsers/Reachable/MaybeEmpty/OfParse.v b/src/Parsers/Reachable/MaybeEmpty/OfParse.v index 9255b36bc..ad7df3398 100644 --- a/src/Parsers/Reachable/MaybeEmpty/OfParse.v +++ b/src/Parsers/Reachable/MaybeEmpty/OfParse.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Every parse tree has a corresponding minimal parse tree *) -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Properties. Require Import Fiat.Parsers.StringLike.Properties. diff --git a/src/Parsers/Reachable/OnlyFirst/MinimalReachable.v b/src/Parsers/Reachable/OnlyFirst/MinimalReachable.v index bda721c83..43db3a5c0 100644 --- a/src/Parsers/Reachable/OnlyFirst/MinimalReachable.v +++ b/src/Parsers/Reachable/OnlyFirst/MinimalReachable.v @@ -1,5 +1,5 @@ (** * Definition of minimal parse trees *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.Reachable.MaybeEmpty.Minimal. Require Import Fiat.Parsers.BaseTypes. diff --git a/src/Parsers/Reachable/OnlyFirst/MinimalReachableOfReachable.v b/src/Parsers/Reachable/OnlyFirst/MinimalReachableOfReachable.v index e51400d72..05fa7aa51 100644 --- a/src/Parsers/Reachable/OnlyFirst/MinimalReachableOfReachable.v +++ b/src/Parsers/Reachable/OnlyFirst/MinimalReachableOfReachable.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Every parse tree has a corresponding minimal parse tree *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import String. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.Reachable.OnlyFirst.Reachable. Require Import Fiat.Parsers.Reachable.OnlyFirst.MinimalReachable. diff --git a/src/Parsers/Reachable/OnlyFirst/Reachable.v b/src/Parsers/Reachable/OnlyFirst/Reachable.v index 382963af9..014a142dd 100644 --- a/src/Parsers/Reachable/OnlyFirst/Reachable.v +++ b/src/Parsers/Reachable/OnlyFirst/Reachable.v @@ -1,5 +1,5 @@ (** * Definition of Context Free Grammars *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Parsers.Reachable.MaybeEmpty.Core. diff --git a/src/Parsers/Reachable/OnlyLast/MinimalReachable.v b/src/Parsers/Reachable/OnlyLast/MinimalReachable.v index 53db101d3..4219f8866 100644 --- a/src/Parsers/Reachable/OnlyLast/MinimalReachable.v +++ b/src/Parsers/Reachable/OnlyLast/MinimalReachable.v @@ -1,5 +1,5 @@ (** * Definition of minimal parse trees *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.Reachable.MaybeEmpty.Minimal. Require Import Fiat.Parsers.BaseTypes. diff --git a/src/Parsers/Reachable/OnlyLast/MinimalReachableOfReachable.v b/src/Parsers/Reachable/OnlyLast/MinimalReachableOfReachable.v index f61c2c19f..5986d656f 100644 --- a/src/Parsers/Reachable/OnlyLast/MinimalReachableOfReachable.v +++ b/src/Parsers/Reachable/OnlyLast/MinimalReachableOfReachable.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Every parse tree has a corresponding minimal parse tree *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import String. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.Reachable.OnlyLast.Reachable. Require Import Fiat.Parsers.Reachable.OnlyLast.MinimalReachable. diff --git a/src/Parsers/Reachable/OnlyLast/Reachable.v b/src/Parsers/Reachable/OnlyLast/Reachable.v index 63da56e81..b9416d60a 100644 --- a/src/Parsers/Reachable/OnlyLast/Reachable.v +++ b/src/Parsers/Reachable/OnlyLast/Reachable.v @@ -1,5 +1,5 @@ (** * Definition of Context Free Grammars *) -Require Import Coq.Strings.String Coq.Lists.List. +From Stdlib Require Import String List. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Parsers.Reachable.MaybeEmpty.Core. diff --git a/src/Parsers/Reachable/OnlyLast/ReachableParse.v b/src/Parsers/Reachable/OnlyLast/ReachableParse.v index 54c526c79..df273f5ee 100644 --- a/src/Parsers/Reachable/OnlyLast/ReachableParse.v +++ b/src/Parsers/Reachable/OnlyLast/ReachableParse.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Every parse tree has a corresponding minimal parse tree *) -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Properties. Require Import Fiat.Parsers.StringLike.LastChar. diff --git a/src/Parsers/Reachable/ParenBalanced/Core.v b/src/Parsers/Reachable/ParenBalanced/Core.v index 3b03ff8a5..45e3430af 100644 --- a/src/Parsers/Reachable/ParenBalanced/Core.v +++ b/src/Parsers/Reachable/ParenBalanced/Core.v @@ -1,6 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Strings.String Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import String List ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Common.List.Operations. diff --git a/src/Parsers/Reachable/ParenBalanced/MinimalOfCore.v b/src/Parsers/Reachable/ParenBalanced/MinimalOfCore.v index 8a1a42d5d..1c8ab0df1 100644 --- a/src/Parsers/Reachable/ParenBalanced/MinimalOfCore.v +++ b/src/Parsers/Reachable/ParenBalanced/MinimalOfCore.v @@ -1,7 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Every parse tree has a corresponding minimal parse tree *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import String ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.Reachable.ParenBalanced.Core. Require Import Fiat.Parsers.Reachable.ParenBalanced.WellFounded. diff --git a/src/Parsers/Reachable/ParenBalanced/OfParse.v b/src/Parsers/Reachable/ParenBalanced/OfParse.v index 272f0661d..dba0d770c 100644 --- a/src/Parsers/Reachable/ParenBalanced/OfParse.v +++ b/src/Parsers/Reachable/ParenBalanced/OfParse.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Every parse tree has a corresponding minimal parse tree *) -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Properties. Require Import Fiat.Parsers.StringLike.Properties. diff --git a/src/Parsers/Reachable/ParenBalancedHiding/Core.v b/src/Parsers/Reachable/ParenBalancedHiding/Core.v index d39d360ef..6abbbb8cc 100644 --- a/src/Parsers/Reachable/ParenBalancedHiding/Core.v +++ b/src/Parsers/Reachable/ParenBalancedHiding/Core.v @@ -1,5 +1,5 @@ -Require Import Coq.Strings.String Coq.Lists.List. -Require Export Coq.Classes.RelationPairs. +From Stdlib Require Import String List. +From Stdlib Require Export RelationPairs. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Parsers.Reachable.ParenBalanced.Core. diff --git a/src/Parsers/Reachable/ParenBalancedHiding/MinimalOfCore.v b/src/Parsers/Reachable/ParenBalancedHiding/MinimalOfCore.v index 5adecc422..96391c2ca 100644 --- a/src/Parsers/Reachable/ParenBalancedHiding/MinimalOfCore.v +++ b/src/Parsers/Reachable/ParenBalancedHiding/MinimalOfCore.v @@ -1,7 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Every parse tree has a corresponding minimal parse tree *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import String ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.Reachable.ParenBalanced.Core. Require Import Fiat.Parsers.Reachable.ParenBalanced.MinimalOfCore. diff --git a/src/Parsers/RecognizerPreOptimized.v b/src/Parsers/RecognizerPreOptimized.v index 43fc5334f..283569932 100644 --- a/src/Parsers/RecognizerPreOptimized.v +++ b/src/Parsers/RecognizerPreOptimized.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import List. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.BaseTypes. diff --git a/src/Parsers/Refinement/BinOpBrackets/BinOpRules.v b/src/Parsers/Refinement/BinOpBrackets/BinOpRules.v index 75130af5e..44c3cabf7 100644 --- a/src/Parsers/Refinement/BinOpBrackets/BinOpRules.v +++ b/src/Parsers/Refinement/BinOpBrackets/BinOpRules.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** Refinement rules for binary operations *) -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import List. +From Stdlib Require Import ZArith. Require Import Fiat.Computation.Refinements.General. Require Import Fiat.Common. Require Import Fiat.Common.Equality. diff --git a/src/Parsers/Refinement/BinOpBrackets/MakeBinOpTable.v b/src/Parsers/Refinement/BinOpBrackets/MakeBinOpTable.v index d9fda10ea..c7574c919 100644 --- a/src/Parsers/Refinement/BinOpBrackets/MakeBinOpTable.v +++ b/src/Parsers/Refinement/BinOpBrackets/MakeBinOpTable.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Build a table for the next binop at a given level *) -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import List. +From Stdlib Require Import ZArith. Require Import Fiat.Common. Require Import Fiat.Common.List.Operations. Require Import Fiat.Common.List.ListFacts. diff --git a/src/Parsers/Refinement/BinOpBrackets/ParenBalanced.v b/src/Parsers/Refinement/BinOpBrackets/ParenBalanced.v index 337adc78b..d9111fa69 100644 --- a/src/Parsers/Refinement/BinOpBrackets/ParenBalanced.v +++ b/src/Parsers/Refinement/BinOpBrackets/ParenBalanced.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Build a table for the next binop at a given level *) -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.Reachable.ParenBalanced.Core. Require Import Fiat.Parsers.StringLike.Core. Require Import Fiat.Parsers.StringLike.Properties. diff --git a/src/Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar.v b/src/Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar.v index 6b5c963c1..c7890cd12 100644 --- a/src/Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar.v +++ b/src/Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms. -Require Import Coq.ZArith.ZArith. +Require Import Stdlib.Lists.List Stdlib.Setoids.Setoid Stdlib.Classes.Morphisms. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.Splitters.RDPList. Require Import Fiat.Parsers.Refinement.BinOpBrackets.ParenBalanced. Require Import Fiat.Parsers.Reachable.ParenBalanced.Core. diff --git a/src/Parsers/Refinement/BinOpBrackets/ParenBalancedLemmas.v b/src/Parsers/Refinement/BinOpBrackets/ParenBalancedLemmas.v index adba62860..1bf108ce6 100644 --- a/src/Parsers/Refinement/BinOpBrackets/ParenBalancedLemmas.v +++ b/src/Parsers/Refinement/BinOpBrackets/ParenBalancedLemmas.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.StringLike.Core. Require Import Fiat.Parsers.StringLike.Properties. Require Import Fiat.Parsers.Reachable.ParenBalanced.Core. diff --git a/src/Parsers/Refinement/DisjointLemmas.v b/src/Parsers/Refinement/DisjointLemmas.v index c5877326a..eb325156f 100644 --- a/src/Parsers/Refinement/DisjointLemmas.v +++ b/src/Parsers/Refinement/DisjointLemmas.v @@ -1,13 +1,13 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** Sharpened ADT for an expression grammar with parentheses *) -Require Import Coq.Init.Wf Coq.Arith.Wf_nat. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List Coq.Strings.String. +Require Import Stdlib.Init.Wf Stdlib.Arith.Wf_nat. +From Stdlib Require Import ZArith. +Require Import Stdlib.Lists.List Stdlib.Strings.String. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.ContextFreeGrammar.Equality. -Require Import Coq.Program.Equality. -Require Import Coq.MSets.MSetPositive. +Require Import Stdlib.Program.Equality. +Require Import Stdlib.MSets.MSetPositive. Require Import Fiat.Common. Require Import Fiat.Common.Equality. Require Import Fiat.Common.Wf. diff --git a/src/Parsers/Refinement/DisjointRules.v b/src/Parsers/Refinement/DisjointRules.v index 96e33892f..f308487b9 100644 --- a/src/Parsers/Refinement/DisjointRules.v +++ b/src/Parsers/Refinement/DisjointRules.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** Refinement rules for disjoint rules *) -Require Import Coq.ZArith.ZArith Coq.Lists.List. +From Stdlib Require Import ZArith List. Require Import Fiat.Parsers.Refinement.PreTactics. Require Import Fiat.Computation.Refinements.General. Require Import Fiat.Parsers.StringLike.Properties. diff --git a/src/Parsers/Refinement/DisjointRulesRev.v b/src/Parsers/Refinement/DisjointRulesRev.v index bbe07e686..4f178378c 100644 --- a/src/Parsers/Refinement/DisjointRulesRev.v +++ b/src/Parsers/Refinement/DisjointRulesRev.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** Refinement rules for disjoint rules *) -Require Import Coq.ZArith.ZArith Coq.Lists.List. +From Stdlib Require Import ZArith List. Require Import Fiat.Parsers.Refinement.PreTactics. Require Import Fiat.Computation.Refinements.General. Require Import Fiat.Parsers.StringLike.LastCharSuchThat. diff --git a/src/Parsers/Refinement/EmptyLemmas.v b/src/Parsers/Refinement/EmptyLemmas.v index edf254431..a62112bbe 100644 --- a/src/Parsers/Refinement/EmptyLemmas.v +++ b/src/Parsers/Refinement/EmptyLemmas.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.StringLike.Properties. diff --git a/src/Parsers/Refinement/ExtractSharpenedJSComment.v b/src/Parsers/Refinement/ExtractSharpenedJSComment.v index 876414dcb..1329fa18e 100644 --- a/src/Parsers/Refinement/ExtractSharpenedJSComment.v +++ b/src/Parsers/Refinement/ExtractSharpenedJSComment.v @@ -14,7 +14,7 @@ Print js_comment_parser_ocaml. Recursive Extraction js_comment_parser_ocaml. (* -Parameter reference_js_comment_parser : Coq.Strings.String.string -> bool. +Parameter reference_js_comment_parser : Stdlib.Strings.String.string -> bool. Parameter reference_js_comment_parser_ocaml : Ocaml.Ocaml.string -> bool. Extract Constant reference_js_comment_parser => "fun str -> diff --git a/src/Parsers/Refinement/ExtractSharpenedJSON.v b/src/Parsers/Refinement/ExtractSharpenedJSON.v index a14a40e7d..9a727da82 100644 --- a/src/Parsers/Refinement/ExtractSharpenedJSON.v +++ b/src/Parsers/Refinement/ExtractSharpenedJSON.v @@ -20,7 +20,7 @@ Print json_parser(*_ocaml*). Definition main_json := premain json_parser. Definition main_json_ocaml := premain_ocaml json_parser_ocaml. -Parameter reference_json_parser : Coq.Strings.String.string -> bool. +Parameter reference_json_parser : Stdlib.Strings.String.string -> bool. Parameter reference_json_parser_ocaml : Ocaml.Ocaml.string -> bool. Extract Constant reference_json_parser => "fun str -> diff --git a/src/Parsers/Refinement/FixedLengthLemmas.v b/src/Parsers/Refinement/FixedLengthLemmas.v index d7b60c313..907148f59 100644 --- a/src/Parsers/Refinement/FixedLengthLemmas.v +++ b/src/Parsers/Refinement/FixedLengthLemmas.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Init.Wf Coq.Arith.Wf_nat. -Require Import Coq.Lists.List Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +Require Import Stdlib.Init.Wf Stdlib.Arith.Wf_nat. +Require Import Stdlib.Lists.List Stdlib.Strings.String. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.ContextFreeGrammar.Precompute. diff --git a/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective.v b/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective.v index 466090eef..ffb136d30 100644 --- a/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective.v +++ b/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** First step of a splitter refinement; indexed representation, and handle all rules with at most one nonterminal; leave a reflective goal *) -Require Import Coq.Strings.String Coq.Arith.PeanoNat Coq.Lists.List. +From Stdlib Require Import String PeanoNat List. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Parsers.Splitters.RDPList. Require Import Fiat.Parsers.ParserInterface. diff --git a/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt.v b/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt.v index ea14bfa14..cade9a9ce 100644 --- a/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt.v +++ b/src/Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt.v @@ -1,5 +1,5 @@ (** First step of a splitter refinement; indexed representation, and handle all rules with at most one nonterminal; leave a reflective goal *) -Require Import Coq.Strings.String. +From Stdlib Require Import String. Require Import Fiat.Common.List.ListFacts. Require Import Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig. Require Import Fiat.ADT.ComputationalADT. diff --git a/src/Parsers/Refinement/PossibleTerminalsSets.v b/src/Parsers/Refinement/PossibleTerminalsSets.v index 5addf816c..3e3e883dc 100644 --- a/src/Parsers/Refinement/PossibleTerminalsSets.v +++ b/src/Parsers/Refinement/PossibleTerminalsSets.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.MSets.MSetPositive. -Require Import Coq.Classes.Morphisms. +Require Import Stdlib.MSets.MSetPositive. +Require Import Stdlib.Classes.Morphisms. Require Import Fiat.Parsers.StringLike.FirstChar Fiat.Parsers.StringLike.LastChar Fiat.Parsers.StringLike.ForallChars. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. diff --git a/src/Parsers/Refinement/PreTactics.v b/src/Parsers/Refinement/PreTactics.v index 0f0f590bb..b2abc4578 100644 --- a/src/Parsers/Refinement/PreTactics.v +++ b/src/Parsers/Refinement/PreTactics.v @@ -1,10 +1,10 @@ Require Export Fiat.Parsers.ContextFreeGrammar.Core. Require Export Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Export Fiat.Parsers.StringLike.FirstCharSuchThat. -Require Export Coq.Strings.String. -Require Export Coq.Arith.PeanoNat. +Require Export Stdlib.Strings.String. +Require Export Stdlib.Arith.PeanoNat. Require Export Fiat.Computation.Core. -Require Export Coq.Program.Program. +Require Export Stdlib.Program.Program. Require Export Fiat.Computation.ApplyMonad. Require Export Fiat.Computation.SetoidMorphisms. Require Export Fiat.Common. @@ -15,7 +15,7 @@ Require Import Fiat.Parsers.ContextFreeGrammar.Carriers. Require Import Fiat.Common.Equality. Require Import Fiat.Common.BoolFacts. Require Import Fiat.Common.NatFacts. -Require Import Coq.Lists.List. +From Stdlib Require Import List. Export Common.opt2.Notations. diff --git a/src/Parsers/Refinement/SharpenedABStar.v b/src/Parsers/Refinement/SharpenedABStar.v index bb9345360..5e5c560df 100644 --- a/src/Parsers/Refinement/SharpenedABStar.v +++ b/src/Parsers/Refinement/SharpenedABStar.v @@ -38,7 +38,7 @@ Require Export Fiat.Parsers.ExtrOcamlParsers. Export Fiat.Parsers.ExtrOcamlParsers.HideProofs. Require Export Fiat.Parsers.StringLike.OcamlString. -Definition ab_star_parser (str : Coq.Strings.String.string) : bool. +Definition ab_star_parser (str : Stdlib.Strings.String.string) : bool. Proof. Time make_parser (@ComputationalSplitter _ String.string_stringlike _ _). (* 0.82 s *) Defined. @@ -55,7 +55,7 @@ Recursive Extraction ab_star_parser_ocaml. Definition main_ab_star := premain ab_star_parser. Definition main_ab_star_ocaml := premain_ocaml ab_star_parser_ocaml. -Parameter reference_ab_star_parser : Coq.Strings.String.string -> bool. +Parameter reference_ab_star_parser : Stdlib.Strings.String.string -> bool. Parameter reference_ab_star_parser_ocaml : Ocaml.Ocaml.string -> bool. Extract Constant reference_ab_star_parser => "fun str -> diff --git a/src/Parsers/Refinement/SharpenedABStarParseTree.v b/src/Parsers/Refinement/SharpenedABStarParseTree.v index f615d3942..968bbfba8 100644 --- a/src/Parsers/Refinement/SharpenedABStarParseTree.v +++ b/src/Parsers/Refinement/SharpenedABStarParseTree.v @@ -9,7 +9,7 @@ Proof. exact b. Defined. -Definition ab_star_parser_informative_opaque (str : Coq.Strings.String.string) +Definition ab_star_parser_informative_opaque (str : Stdlib.Strings.String.string) : option (parse_of_item ab_star_grammar str (NonTerminal (Start_symbol ab_star_grammar))). Proof. Time make_parser_informative_opaque (@ComputationalSplitter _ String.string_stringlike _ _). (* 0.82 s *) @@ -23,7 +23,7 @@ Proof. change (LHS = b). Abort. -Definition ab_star_parser_informative (str : Coq.Strings.String.string) +Definition ab_star_parser_informative (str : Stdlib.Strings.String.string) : option (@simple_parse_of_item Ascii.ascii). Proof. Time make_parser_informative (@ComputationalSplitter _ String.string_stringlike _ _). (* 0.124 s *) diff --git a/src/Parsers/Refinement/SharpenedExpressionPlusParenParseTree.v b/src/Parsers/Refinement/SharpenedExpressionPlusParenParseTree.v index 229b3661e..68296be97 100644 --- a/src/Parsers/Refinement/SharpenedExpressionPlusParenParseTree.v +++ b/src/Parsers/Refinement/SharpenedExpressionPlusParenParseTree.v @@ -5,19 +5,19 @@ Require Import Fiat.Parsers.ActionEvaluator. Require Import Fiat.Parsers.Refinement.SharpenedExpressionPlusParen. Require Import Fiat.Parsers.Grammars.EvalGrammarTactics. -Definition parser_informative_opaque (str : Coq.Strings.String.string) +Definition parser_informative_opaque (str : Stdlib.Strings.String.string) : option (parse_of_item plus_expr_grammar str (NonTerminal (Start_symbol plus_expr_grammar))). Proof. Time make_parser_informative_opaque ComputationalSplitter. Defined. -Definition parser_informative (str : Coq.Strings.String.string) +Definition parser_informative (str : Stdlib.Strings.String.string) : option (@simple_parse_of_item Ascii.ascii). Proof. Time make_parser_informative ComputationalSplitter. Defined. -Definition parser_eval (str : Coq.Strings.String.string) +Definition parser_eval (str : Stdlib.Strings.String.string) : option nat. Proof. refine match parser_informative str with diff --git a/src/Parsers/Refinement/SharpenedJSComment.v b/src/Parsers/Refinement/SharpenedJSComment.v index 9c0d8cb9d..6959ca8f7 100644 --- a/src/Parsers/Refinement/SharpenedJSComment.v +++ b/src/Parsers/Refinement/SharpenedJSComment.v @@ -90,7 +90,7 @@ Require Export Fiat.Parsers.ExtrOcamlParsers. Export Fiat.Parsers.ExtrOcamlParsers.HideProofs. Require Export Fiat.Parsers.StringLike.OcamlString. -Definition js_comment_parser (str : Coq.Strings.String.string) : bool. +Definition js_comment_parser (str : Stdlib.Strings.String.string) : bool. Proof. Time make_parser (@ComputationalSplitter _ String.string_stringlike _ _). (* 0.82 s *) Defined. @@ -103,7 +103,7 @@ Defined. Definition main_js_comment := premain js_comment_parser. Definition main_js_comment_ocaml := premain_ocaml js_comment_parser_ocaml. (* -Parameter reference_js_comment_parser : Coq.Strings.String.string -> bool. +Parameter reference_js_comment_parser : Stdlib.Strings.String.string -> bool. Parameter reference_js_comment_parser_ocaml : Ocaml.Ocaml.string -> bool. Extract Constant reference_js_comment_parser => "fun str -> diff --git a/src/Parsers/Refinement/SharpenedJSON.v b/src/Parsers/Refinement/SharpenedJSON.v index d2a23108f..88897976d 100644 --- a/src/Parsers/Refinement/SharpenedJSON.v +++ b/src/Parsers/Refinement/SharpenedJSON.v @@ -133,7 +133,7 @@ Require Export Fiat.Parsers.ExtrOcamlParsers. Export Fiat.Parsers.ExtrOcamlParsers.HideProofs. Require Export Fiat.Parsers.StringLike.OcamlString. -Definition json_parser (str : Coq.Strings.String.string) : bool. +Definition json_parser (str : Stdlib.Strings.String.string) : bool. Proof. (*Start Profiling.*) Time make_parser (@ComputationalSplitter(* _ String.string_stringlike _ _*)). (* 75 seconds *) @@ -150,7 +150,7 @@ Defined.*) Definition main_json := premain json_parser. Definition main_json_ocaml := premain_ocaml json_parser_ocaml. -Parameter reference_json_parser : Coq.Strings.String.string -> bool. +Parameter reference_json_parser : Stdlib.Strings.String.string -> bool. Parameter reference_json_parser_ocaml : Ocaml.Ocaml.string -> bool. Extract Constant reference_json_parser => "fun str -> diff --git a/src/Parsers/Refinement/SharpenedJavaScriptAssignmentExpression.v b/src/Parsers/Refinement/SharpenedJavaScriptAssignmentExpression.v index d89e06edf..ecc7293eb 100644 --- a/src/Parsers/Refinement/SharpenedJavaScriptAssignmentExpression.v +++ b/src/Parsers/Refinement/SharpenedJavaScriptAssignmentExpression.v @@ -7,13 +7,13 @@ Require Import Fiat.Parsers.ExtrOcamlParsers. (* for simpl rules for [find_first Require Import Fiat.Parsers.Refinement.BinOpBrackets.BinOpRules. Require Import Fiat.Parsers.StringLike.String. -(*Require Coq.micromega.Lia. -Require Coq.PArith.BinPos. -Require Coq.Lists.List. -Require Coq.Sorting.Mergesort. -Require Coq.Structures.OrdersEx. -Require Coq.Strings.Ascii. -Require Coq.Strings.String. +(*Require Stdlib.micromega.Lia. +Require Stdlib.PArith.BinPos. +Require Stdlib.Lists.List. +Require Stdlib.Sorting.Mergesort. +Require Stdlib.Structures.OrdersEx. +Require Stdlib.Strings.Ascii. +Require Stdlib.Strings.String. Require Fiat.Parsers.ContextFreeGrammar.Core. Require Fiat.Parsers.ContextFreeGrammar.Carriers. Require Fiat.Parsers.ContextFreeGrammar.Reflective. @@ -310,7 +310,7 @@ Require Export Fiat.Parsers.ExtrOcamlParsers. Export Fiat.Parsers.ExtrOcamlParsers.HideProofs. Require Export Fiat.Parsers.StringLike.OcamlString. -Definition json_parser (str : Coq.Strings.String.string) : bool. +Definition json_parser (str : Stdlib.Strings.String.string) : bool. Proof. Reset Ltac Profiling. Time make_parser (@ComputationalSplitter(* _ String.string_stringlike _ _*)). (* 75 seconds *) @@ -329,7 +329,7 @@ Recursive Extraction json_parser(*_ocaml*). Definition main_json := premain json_parser. Definition main_json_ocaml := premain_ocaml json_parser_ocaml. -Parameter reference_json_parser : Coq.Strings.String.string -> bool. +Parameter reference_json_parser : Stdlib.Strings.String.string -> bool. Parameter reference_json_parser_ocaml : Ocaml.Ocaml.string -> bool. Extract Constant reference_json_parser => "fun str -> diff --git a/src/Parsers/Refinement/SharpenedStringLiteral.v b/src/Parsers/Refinement/SharpenedStringLiteral.v index da7bc1792..52e3b00bb 100644 --- a/src/Parsers/Refinement/SharpenedStringLiteral.v +++ b/src/Parsers/Refinement/SharpenedStringLiteral.v @@ -27,7 +27,7 @@ Require Export Fiat.Parsers.ExtrOcamlParsers. Export Fiat.Parsers.ExtrOcamlParsers.HideProofs. Require Export Fiat.Parsers.StringLike.OcamlString. -Definition string_parser (str : Coq.Strings.String.string) : bool. +Definition string_parser (str : Stdlib.Strings.String.string) : bool. Proof. Time make_parser (@ComputationalSplitter _ String.string_stringlike _ _). (* 0.82 s *) Defined. @@ -44,7 +44,7 @@ Recursive Extraction string_parser_ocaml. Definition main_string := premain string_parser. Definition main_string_ocaml := premain_ocaml string_parser_ocaml. (* -Parameter reference_string_parser : Coq.Strings.String.string -> bool. +Parameter reference_string_parser : Stdlib.Strings.String.string -> bool. Parameter reference_string_parser_ocaml : Ocaml.Ocaml.string -> bool. Extract Constant reference_string_parser => "fun str -> diff --git a/src/Parsers/Refinement/Tactics.v b/src/Parsers/Refinement/Tactics.v index b3568b837..8e7c5bcf2 100644 --- a/src/Parsers/Refinement/Tactics.v +++ b/src/Parsers/Refinement/Tactics.v @@ -1,4 +1,4 @@ -Require Export Coq.NArith.BinNat. +Require Export Stdlib.NArith.BinNat. Require Export Fiat.ADTRefinement. Require Export Fiat.ADTNotation.BuildADT. Require Export Fiat.ADTRefinement.GeneralBuildADTRefinements. diff --git a/src/Parsers/Reflective/LogicalRelations.v b/src/Parsers/Reflective/LogicalRelations.v index 58d309c2f..24f72e53b 100644 --- a/src/Parsers/Reflective/LogicalRelations.v +++ b/src/Parsers/Reflective/LogicalRelations.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Classes.Morphisms. +From Stdlib Require Import ZArith. +Require Import Stdlib.Classes.Morphisms. Require Import Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics. Require Import Fiat.Parsers.Reflective.PartialUnfold. Require Import Fiat.Parsers.Reflective.SyntaxEquivalence. diff --git a/src/Parsers/Reflective/Morphisms.v b/src/Parsers/Reflective/Morphisms.v index 1ae853c98..7f9c508dd 100644 --- a/src/Parsers/Reflective/Morphisms.v +++ b/src/Parsers/Reflective/Morphisms.v @@ -1,4 +1,4 @@ -Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions. +Require Import Stdlib.Classes.Morphisms Stdlib.Relations.Relation_Definitions. Require Import Fiat.Parsers.Reflective.Syntax. Require Import Fiat.Parsers.Reflective.Semantics. Require Import Fiat.Common.List.ListMorphisms. diff --git a/src/Parsers/Reflective/ParserLogicalRelations.v b/src/Parsers/Reflective/ParserLogicalRelations.v index e4fb184be..9f84caab4 100644 --- a/src/Parsers/Reflective/ParserLogicalRelations.v +++ b/src/Parsers/Reflective/ParserLogicalRelations.v @@ -1,4 +1,4 @@ -Require Import Coq.Classes.Morphisms. +Require Import Stdlib.Classes.Morphisms. Require Import Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics. Require Import Fiat.Parsers.Reflective.PartialUnfold. Require Import Fiat.Parsers.Reflective.ParserSyntax Fiat.Parsers.Reflective.ParserSemantics. diff --git a/src/Parsers/Reflective/ParserSemantics.v b/src/Parsers/Reflective/ParserSemantics.v index 24b8764e3..3c888f31f 100644 --- a/src/Parsers/Reflective/ParserSemantics.v +++ b/src/Parsers/Reflective/ParserSemantics.v @@ -3,7 +3,7 @@ Require Import Fiat.Parsers.Reflective.Semantics. Require Import Fiat.Parsers.Splitters.RDPList. Require Import Fiat.Parsers.GenericRecognizer. Require Import Fiat.Common.Wf Fiat.Common.Wf2. -Require Import Coq.Arith.PeanoNat. +Require Import Stdlib.Arith.PeanoNat. Set Implicit Arguments. Definition step_option_rec diff --git a/src/Parsers/Reflective/Reify.v b/src/Parsers/Reflective/Reify.v index 07dd10765..e40219173 100644 --- a/src/Parsers/Reflective/Reify.v +++ b/src/Parsers/Reflective/Reify.v @@ -1,5 +1,5 @@ -Require Export Coq.Strings.String. (* for error messages *) -Require Import Coq.Strings.Ascii. +Require Export Stdlib.Strings.String. (* for error messages *) +Require Import Stdlib.Strings.Ascii. Require Import Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics. Require Import Fiat.Parsers.Reflective.Syntactify. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. @@ -301,6 +301,6 @@ Hint Extern 0 (reif_Term_of ?var ?term) Module Exports. Export Syntax.Coercions. - Export Coq.Strings.String. + Export Stdlib.Strings.String. Open Scope string_scope. End Exports. diff --git a/src/Parsers/Reflective/Semantics.v b/src/Parsers/Reflective/Semantics.v index 6ba082192..6364eefb6 100644 --- a/src/Parsers/Reflective/Semantics.v +++ b/src/Parsers/Reflective/Semantics.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String. +From Stdlib Require Import String. Require Import Fiat.Parsers.Reflective.Syntax. Require Import Fiat.Parsers.Reflective.Syntactify. Require Import Fiat.Common.NatFacts. diff --git a/src/Parsers/Reflective/Syntactify.v b/src/Parsers/Reflective/Syntactify.v index ff3d269c6..ddcd96e00 100644 --- a/src/Parsers/Reflective/Syntactify.v +++ b/src/Parsers/Reflective/Syntactify.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.Strings.Ascii. +From Stdlib Require Import String Ascii. Require Import Fiat.Parsers.Reflective.Syntax. Set Implicit Arguments. diff --git a/src/Parsers/Reflective/Syntax.v b/src/Parsers/Reflective/Syntax.v index 65a2b1c61..402ee5ad8 100644 --- a/src/Parsers/Reflective/Syntax.v +++ b/src/Parsers/Reflective/Syntax.v @@ -1,5 +1,5 @@ -Require Import Coq.Classes.Morphisms. (* for reserved [-->] notation *) -Require Import Coq.Strings.String Coq.Strings.Ascii. +Require Import Stdlib.Classes.Morphisms. (* for reserved [-->] notation *) +From Stdlib Require Import String Ascii. Require Import Fiat.Parsers.ContextFreeGrammar.Reflective. Require Import Fiat.Common.Notations. diff --git a/src/Parsers/Reflective/SyntaxEquality.v b/src/Parsers/Reflective/SyntaxEquality.v index 5b019a997..bc168a108 100644 --- a/src/Parsers/Reflective/SyntaxEquality.v +++ b/src/Parsers/Reflective/SyntaxEquality.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.Ascii. +Require Import Stdlib.Strings.Ascii. Require Import Fiat.Parsers.Reflective.Syntax. Require Import Fiat.Parsers.ContextFreeGrammar.Reflective. Require Import Fiat.Common.Equality. diff --git a/src/Parsers/Reflective/SyntaxEquivalence.v b/src/Parsers/Reflective/SyntaxEquivalence.v index 91e3c18e6..cc1a9ee13 100644 --- a/src/Parsers/Reflective/SyntaxEquivalence.v +++ b/src/Parsers/Reflective/SyntaxEquivalence.v @@ -1,5 +1,5 @@ (** * Equivalence on syntax *) -Require Import Coq.Lists.List. +From Stdlib Require Import List. Require Import Fiat.Parsers.Reflective.Syntax. Local Open Scope list_scope. diff --git a/src/Parsers/Reflective/SyntaxEquivalenceReflective.v b/src/Parsers/Reflective/SyntaxEquivalenceReflective.v index 693c35103..c270740eb 100644 --- a/src/Parsers/Reflective/SyntaxEquivalenceReflective.v +++ b/src/Parsers/Reflective/SyntaxEquivalenceReflective.v @@ -1,6 +1,6 @@ (** * Equivalence on syntax *) -Require Import Coq.Lists.List. -Require Import Coq.Arith.EqNat Coq.Logic.Eqdep_dec. +From Stdlib Require Import List. +Require Import Stdlib.Arith.EqNat Stdlib.Logic.Eqdep_dec. Require Import Fiat.Parsers.Reflective.Syntax. Require Import Fiat.Parsers.Reflective.SyntaxEquality. Require Import Fiat.Parsers.Reflective.SyntaxEquivalence. diff --git a/src/Parsers/SimpleRecognizerCorrect.v b/src/Parsers/SimpleRecognizerCorrect.v index 1c042a53d..815209ef5 100644 --- a/src/Parsers/SimpleRecognizerCorrect.v +++ b/src/Parsers/SimpleRecognizerCorrect.v @@ -1,5 +1,5 @@ (** * Proof that SimpleRecognizer outputs correct parse trees *) -Require Import Coq.Classes.Morphisms Coq.Arith.PeanoNat. +Require Import Stdlib.Classes.Morphisms Stdlib.Arith.PeanoNat. Require Import Fiat.Parsers.StringLike.Core. Require Import Fiat.Parsers.StringLike.Properties. Require Import Fiat.Parsers.ContextFreeGrammar.Core. diff --git a/src/Parsers/SimpleRecognizerExt.v b/src/Parsers/SimpleRecognizerExt.v index 75d2b027a..d783e4afb 100644 --- a/src/Parsers/SimpleRecognizerExt.v +++ b/src/Parsers/SimpleRecognizerExt.v @@ -1,5 +1,5 @@ (** * Extensionality of simple recognizer *) -Require Import Coq.Classes.Morphisms. +Require Import Stdlib.Classes.Morphisms. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.BaseTypes. Require Import Fiat.Parsers.SimpleRecognizer. diff --git a/src/Parsers/SplitterFromParserADT.v b/src/Parsers/SplitterFromParserADT.v index 81b2bde66..f4a28c708 100644 --- a/src/Parsers/SplitterFromParserADT.v +++ b/src/Parsers/SplitterFromParserADT.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (*Reference implementation of a splitter and parser based on that splitter *) -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import String. +From Stdlib Require Import ZArith. Require Import Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig. Require Import Fiat.ADT.ComputationalADT. Require Import Fiat.ADTRefinement.GeneralRefinements. diff --git a/src/Parsers/Splitters/BruteForce.v b/src/Parsers/Splitters/BruteForce.v index 1f3afa1c5..275236c12 100644 --- a/src/Parsers/Splitters/BruteForce.v +++ b/src/Parsers/Splitters/BruteForce.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Definition of a boolean-returning CFG parser-recognizer *) -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import List. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.BaseTypes Fiat.Parsers.CorrectnessBaseTypes. diff --git a/src/Parsers/Splitters/RDPList.v b/src/Parsers/Splitters/RDPList.v index 163604cd8..602d2a96e 100644 --- a/src/Parsers/Splitters/RDPList.v +++ b/src/Parsers/Splitters/RDPList.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Definition of the part of boolean-returning CFG parser-recognizer that instantiates things to lists *) -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import List. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.PreNotations. Require Import Fiat.Parsers.BaseTypes. diff --git a/src/Parsers/StringLike/Core.v b/src/Parsers/StringLike/Core.v index f3fc319f8..d33204d28 100644 --- a/src/Parsers/StringLike/Core.v +++ b/src/Parsers/StringLike/Core.v @@ -1,7 +1,7 @@ (** * Definition of the string-like type *) -Require Coq.Lists.List. -Require Import Coq.Relations.Relation_Definitions (* for [relation] *). -Require Import Coq.Classes.Morphisms (* for [==>] / [respectful] *). +From Stdlib Require List. +From Stdlib Require Import Relation_Definitions (* for [relation] *). +From Stdlib Require Import Morphisms (* for [==>] / [respectful] *). Require Export Fiat.Common.Coq__8_4__8_5__Compat. Local Coercion is_true : bool >-> Sortclass. diff --git a/src/Parsers/StringLike/FirstChar.v b/src/Parsers/StringLike/FirstChar.v index d3d821265..16e4b93bc 100644 --- a/src/Parsers/StringLike/FirstChar.v +++ b/src/Parsers/StringLike/FirstChar.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Mapping predicates over [StringLike] things *) -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.StringLike.Core. Require Import Fiat.Parsers.StringLike.Properties. Require Import Fiat.Parsers.StringLike.ForallChars. diff --git a/src/Parsers/StringLike/FirstCharSuchThat.v b/src/Parsers/StringLike/FirstCharSuchThat.v index c21133931..a6f9092e3 100644 --- a/src/Parsers/StringLike/FirstCharSuchThat.v +++ b/src/Parsers/StringLike/FirstCharSuchThat.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Mapping predicates over [StringLike] things *) -Require Import Coq.Arith.PeanoNat. +From Stdlib Require Import PeanoNat. Require Import Fiat.Parsers.StringLike.Core. Require Import Fiat.Parsers.StringLike.Properties. Require Import Fiat.Parsers.StringLike.ForallChars. diff --git a/src/Parsers/StringLike/ForallChars.v b/src/Parsers/StringLike/ForallChars.v index eb2e7023c..3727c62cb 100644 --- a/src/Parsers/StringLike/ForallChars.v +++ b/src/Parsers/StringLike/ForallChars.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Mapping predicates over [StringLike] things *) -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.StringLike.Core. Require Import Fiat.Parsers.StringLike.Properties. Require Import Fiat.Common. diff --git a/src/Parsers/StringLike/LastChar.v b/src/Parsers/StringLike/LastChar.v index 6dc453f99..82dcf0a87 100644 --- a/src/Parsers/StringLike/LastChar.v +++ b/src/Parsers/StringLike/LastChar.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Mapping predicates over [StringLike] things *) -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.StringLike.Core. Require Import Fiat.Parsers.StringLike.Properties. Require Import Fiat.Parsers.StringLike.ForallChars. diff --git a/src/Parsers/StringLike/LastCharSuchThat.v b/src/Parsers/StringLike/LastCharSuchThat.v index 5b7d1f24e..4b0771f00 100644 --- a/src/Parsers/StringLike/LastCharSuchThat.v +++ b/src/Parsers/StringLike/LastCharSuchThat.v @@ -1,6 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Mapping predicates over [StringLike] things *) -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Parsers.StringLike.Core. Require Import Fiat.Parsers.StringLike.Properties. Require Import Fiat.Parsers.StringLike.ForallChars. diff --git a/src/Parsers/StringLike/OcamlString.v b/src/Parsers/StringLike/OcamlString.v index 83e6a13f3..84490e968 100644 --- a/src/Parsers/StringLike/OcamlString.v +++ b/src/Parsers/StringLike/OcamlString.v @@ -1,8 +1,8 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Strings.Ascii. -Require Import Coq.Strings.String. -Require Import Coq.ZArith.BinInt. +From Stdlib Require Import ZArith. +Require Import Stdlib.Strings.Ascii. +From Stdlib Require Import String. +Require Import Stdlib.ZArith.BinInt. Require Import Fiat.Common.Equality. Require Import Fiat.Common.StringOperations. Require Import Fiat.Common.StringFacts. @@ -22,18 +22,18 @@ Local Ltac t' := | [ |- is_true false ] => exfalso | _ => progress autorewrite with ocaml in * | [ s : Ocaml.string |- _ ] => generalize dependent (Ocaml.explode s); clear s - | [ |- Coq.Strings.String.get _ (string_of_list _) = List.nth_error _ _ ] + | [ |- Stdlib.Strings.String.get _ (string_of_list _) = List.nth_error _ _ ] => apply get_string_of_list | _ => progress simpl in * | _ => progress subst | [ H : context[string_eq_dec ?x ?y] |- _ ] => destruct (string_eq_dec x y) | [ H : context[ascii_eq_dec ?x ?y] |- _ ] => destruct (ascii_eq_dec x y) - | [ H : Coq.Strings.String.String _ _ = Coq.Strings.String.String _ _ |- _ ] => inversion H; clear H + | [ H : Stdlib.Strings.String.String _ _ = Stdlib.Strings.String.String _ _ |- _ ] => inversion H; clear H | [ H : is_true false |- _ ] => exfalso; clear -H; hnf in H; discriminate | _ => progress unfold beq in * | _ => rewrite string_dec_refl | [ |- RelationClasses.Equivalence _ ] => split - | [ H : Coq.Strings.String.length ?s = 0 |- _ ] => atomic s; destruct s + | [ H : Stdlib.Strings.String.length ?s = 0 |- _ ] => atomic s; destruct s | _ => exfalso; congruence | _ => rewrite substring_length | _ => rewrite <- plus_n_O @@ -63,19 +63,19 @@ Local Ltac t' := | [ |- context[string_eq_dec ?x ?y] ] => destruct (string_eq_dec x y) | [ H : _ <> _ |- False ] => apply H; clear H | _ => apply Nat.max_case_strong; intro; apply substring_correct4; omega - | [ H : Coq.Strings.String.length ?s = 1 |- _ ] => is_var s; destruct s - | [ H : S (Coq.Strings.String.length ?s) = 1 |- _ ] => is_var s; destruct s + | [ H : Stdlib.Strings.String.length ?s = 1 |- _ ] => is_var s; destruct s + | [ H : S (Stdlib.Strings.String.length ?s) = 1 |- _ ] => is_var s; destruct s | _ => eexists; rewrite (ascii_lb eq_refl); reflexivity | [ |- _ <-> _ ] => split - | [ H : Coq.Strings.String.get 0 ?s = _ |- _ ] => is_var s; destruct s - | [ |- Coq.Strings.String.get 0 ?s = _ ] => is_var s; destruct s + | [ H : Stdlib.Strings.String.get 0 ?s = _ |- _ ] => is_var s; destruct s + | [ |- Stdlib.Strings.String.get 0 ?s = _ ] => is_var s; destruct s | [ H : Some _ = Some _ |- _ ] => inversion H; clear H - | [ |- context[Coq.Strings.String.get ?p (Coq.Strings.String.substring _ ?m _)] ] + | [ |- context[Stdlib.Strings.String.get ?p (Stdlib.Strings.String.substring _ ?m _)] ] => destruct (Compare_dec.lt_dec p m); [ rewrite substring_correct1 by omega | rewrite substring_correct2 by omega ] | _ => rewrite <- substring_correct3'; apply substring_correct2; omega - | [ H : forall n, Coq.Strings.String.get n _ = Coq.Strings.String.get n _ |- _ ] => apply get_correct in H + | [ H : forall n, Stdlib.Strings.String.get n _ = Stdlib.Strings.String.get n _ |- _ ] => apply get_correct in H | [ H : Nat.eqb _ _ = true |- _ ] => apply (proj1 (Nat.eqb_eq _ _)) in H | [ H : Nat.eqb _ _ = false |- _ ] => apply (proj1 (Nat.eqb_neq _ _)) in H | [ H : context[Nat.eqb ?x ?y] |- _ ] => destruct (Nat.eqb x y) eqn:? @@ -100,7 +100,7 @@ Local Ltac t' := | [ H' : Strings.String.get ?n (Ocaml.explode ?s) = Some _ |- context[String.get ?s ?n] ] => rewrite (proj2 (@StringProperties.get_correct s n _) H') | [ H : forall n, String.safe_get ?str n = String.safe_get ?str' n |- _ ] - => assert (forall n, Coq.Strings.String.get n (Ocaml.explode str) = Coq.Strings.String.get n (Ocaml.explode str')) + => assert (forall n, Stdlib.Strings.String.get n (Ocaml.explode str) = Stdlib.Strings.String.get n (Ocaml.explode str')) by (intro n; specialize (H n); autorewrite with ocaml in H; exact H); clear H | [ |- String.substring ?n ?m ?s = String.substring ?n ?m' ?s ] diff --git a/src/Parsers/StringLike/Properties.v b/src/Parsers/StringLike/Properties.v index 56bd38370..cd69bae19 100644 --- a/src/Parsers/StringLike/Properties.v +++ b/src/Parsers/StringLike/Properties.v @@ -1,7 +1,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Theorems about string-like types *) -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Import Fiat.Common. Require Import Fiat.Common.List.Operations. Require Import Fiat.Common.List.ListFacts. diff --git a/src/Parsers/StringLike/String.v b/src/Parsers/StringLike/String.v index f4cf71e53..05c1f9a80 100644 --- a/src/Parsers/StringLike/String.v +++ b/src/Parsers/StringLike/String.v @@ -1,9 +1,6 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. (** * Definitions of some specific string-like types *) -Require Import Coq.Strings.Ascii. -Require Import Coq.Strings.String. -Require Import Coq.ZArith.ZArith. -Require Import Coq.Arith.PeanoNat. +From Stdlib Require Import Ascii String ZArith PeanoNat. Require Import Fiat.Common Fiat.Common.Equality. Require Import Fiat.Common.StringOperations Fiat.Common.StringFacts. Require Import Fiat.Parsers.StringLike.Core. diff --git a/src/Parsers/WellFoundedParse.v b/src/Parsers/WellFoundedParse.v index 490b9fc53..df1178d86 100644 --- a/src/Parsers/WellFoundedParse.v +++ b/src/Parsers/WellFoundedParse.v @@ -1,5 +1,5 @@ (** * Well-founded relation on [parse_of] *) -Require Import Coq.Strings.String Coq.Arith.Wf_nat Coq.Relations.Relation_Definitions. +From Stdlib Require Import String Wf_nat Relation_Definitions. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Section rel. diff --git a/src/Parsers/WellFoundedParseProperties.v b/src/Parsers/WellFoundedParseProperties.v index b6c878b63..937d25448 100644 --- a/src/Parsers/WellFoundedParseProperties.v +++ b/src/Parsers/WellFoundedParseProperties.v @@ -1,6 +1,5 @@ (** * Properties about well-founded relation on [parse_of] *) -Require Import Coq.Strings.String Coq.Lists.List Coq.Program.Program. -Require Import Coq.Classes.Morphisms. +From Stdlib Require Import String List Program Morphisms. Require Import Fiat.Parsers.ContextFreeGrammar.Core. Require Import Fiat.Parsers.ContextFreeGrammar.Equality. Require Import Fiat.Parsers.ContextFreeGrammar.Properties. diff --git a/src/QueryStructure/Automation/AutoDB.v b/src/QueryStructure/Automation/AutoDB.v index 62413f3dd..e6402d51a 100644 --- a/src/QueryStructure/Automation/AutoDB.v +++ b/src/QueryStructure/Automation/AutoDB.v @@ -1,4 +1,4 @@ -Require Export Coq.Bool.Bool Coq.Strings.String Coq.Strings.Ascii. +Require Export Stdlib.Bool.Bool Stdlib.Strings.String Stdlib.Strings.Ascii. Require Export Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.Common.BoolFacts @@ -33,7 +33,7 @@ Require Export Fiat.Common.DecideableEnsembles Fiat.QueryStructure.Automation.Common Fiat.QueryStructure.Implementation.Operations. -Require Import Coq.Logic.Eqdep_dec +Require Import Stdlib.Logic.Eqdep_dec Fiat.ADT.ComputationalADT Fiat.ADTNotation.BuildComputationalADT Fiat.ADTRefinement.GeneralBuildADTRefinements. diff --git a/src/QueryStructure/Automation/Common.v b/src/QueryStructure/Automation/Common.v index ef2d80fb5..7d5544cf6 100644 --- a/src/QueryStructure/Automation/Common.v +++ b/src/QueryStructure/Automation/Common.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Fiat.Common Fiat.Common.StringBound Fiat.Common.Tactics.CacheStringConstant diff --git a/src/QueryStructure/Automation/Constraints/ForeignKeyAutomation.v b/src/QueryStructure/Automation/Constraints/ForeignKeyAutomation.v index 6f02066c7..d7b6ccab0 100644 --- a/src/QueryStructure/Automation/Constraints/ForeignKeyAutomation.v +++ b/src/QueryStructure/Automation/Constraints/ForeignKeyAutomation.v @@ -1,5 +1,5 @@ Require Export Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.Operations.Query. -Require Import Coq.Lists.List Coq.Arith.Compare_dec Coq.Bool.Bool Coq.Strings.String +Require Import Stdlib.Lists.List Stdlib.Arith.Compare_dec Stdlib.Bool.Bool Stdlib.Strings.String Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms diff --git a/src/QueryStructure/Automation/Constraints/FunctionalDependencyAutomation.v b/src/QueryStructure/Automation/Constraints/FunctionalDependencyAutomation.v index 24e6a6508..58dd5aab7 100644 --- a/src/QueryStructure/Automation/Constraints/FunctionalDependencyAutomation.v +++ b/src/QueryStructure/Automation/Constraints/FunctionalDependencyAutomation.v @@ -1,9 +1,9 @@ Require Export Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.Operations.Query. -Require Import Coq.Lists.List +Require Import Stdlib.Lists.List Coq.Arith.Compare_dec Coq.Bool.Bool - Coq.Strings.String + Stdlib.Strings.String Coq.Strings.Ascii Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts diff --git a/src/QueryStructure/Automation/Constraints/TrivialConstraintAutomation.v b/src/QueryStructure/Automation/Constraints/TrivialConstraintAutomation.v index dbc636c18..89afe6cfe 100644 --- a/src/QueryStructure/Automation/Constraints/TrivialConstraintAutomation.v +++ b/src/QueryStructure/Automation/Constraints/TrivialConstraintAutomation.v @@ -1,5 +1,5 @@ Require Export Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.Operations.Query. -Require Import Coq.Lists.List Coq.Arith.Compare_dec Coq.Bool.Bool Coq.Strings.String +Require Import Stdlib.Lists.List Stdlib.Arith.Compare_dec Stdlib.Bool.Bool Stdlib.Strings.String Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms diff --git a/src/QueryStructure/Automation/General/DeleteAutomation.v b/src/QueryStructure/Automation/General/DeleteAutomation.v index 5ac9564a6..47abee903 100644 --- a/src/QueryStructure/Automation/General/DeleteAutomation.v +++ b/src/QueryStructure/Automation/General/DeleteAutomation.v @@ -1,5 +1,5 @@ -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles - Fiat.Common.List.ListFacts +From Stdlib Require Import wString ZArith List FunctionalExtensionality Ensembles. +Require Import Fiat.Common.List.ListFacts Fiat.Computation Fiat.Common.Tactics.CacheStringConstant Fiat.ADT diff --git a/src/QueryStructure/Automation/General/InsertAutomation.v b/src/QueryStructure/Automation/General/InsertAutomation.v index eee7e9ee2..0ef12cfe6 100644 --- a/src/QueryStructure/Automation/General/InsertAutomation.v +++ b/src/QueryStructure/Automation/General/InsertAutomation.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List +From Stdlib Require Import String ZArith List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Computation Fiat.ADT diff --git a/src/QueryStructure/Automation/General/QueryAutomation.v b/src/QueryStructure/Automation/General/QueryAutomation.v index 5fa9343b5..52b15296f 100644 --- a/src/QueryStructure/Automation/General/QueryAutomation.v +++ b/src/QueryStructure/Automation/General/QueryAutomation.v @@ -1,7 +1,5 @@ -Require Import Coq.Strings.String Coq.Lists.List Coq.Sorting.Permutation - Coq.Bool.Bool Coq.Sets.Ensembles - Coq.Logic.FunctionalExtensionality - Fiat.ADTNotation Fiat.Common +From Stdlib Require Import String List Permutation Bool Coq.Sets.Ensembles FunctionalExtensionality. +Require Import Fiat.ADTNotation Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles diff --git a/src/QueryStructure/Automation/General/QueryStructureAutomation.v b/src/QueryStructure/Automation/General/QueryStructureAutomation.v index d0ba1b668..41b0f7a5b 100644 --- a/src/QueryStructure/Automation/General/QueryStructureAutomation.v +++ b/src/QueryStructure/Automation/General/QueryStructureAutomation.v @@ -1,6 +1,5 @@ -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles - Coq.Sorting.Permutation - Fiat.Computation +From Stdlib Require Import String ZArith List FunctionalExtensionality Ensembles Permutation. +Require Import Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation diff --git a/src/QueryStructure/Automation/IndexSelection.v b/src/QueryStructure/Automation/IndexSelection.v index 1e6a369fa..c11a04dc9 100644 --- a/src/QueryStructure/Automation/IndexSelection.v +++ b/src/QueryStructure/Automation/IndexSelection.v @@ -1,9 +1,9 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Sorting.Mergesort +Require Import Stdlib.Sorting.Mergesort Coq.Structures.Orders Coq.Arith.Arith Coq.Structures.OrderedType Coq.Structures.OrderedTypeEx - Coq.Strings.String Coq.FSets.FMapAVL + Stdlib.Strings.String Coq.FSets.FMapAVL Fiat.Common.String_as_OT Fiat.Common.Tactics.CacheStringConstant Fiat.QueryStructure.Specification.Representation.QueryStructureNotations diff --git a/src/QueryStructure/Automation/QSImplementation.v b/src/QueryStructure/Automation/QSImplementation.v index 68c57daa2..5a097c0a8 100644 --- a/src/QueryStructure/Automation/QSImplementation.v +++ b/src/QueryStructure/Automation/QSImplementation.v @@ -1,5 +1,5 @@ (* Tactics for extracting Query Structure Implementations. *) -Require Import Coq.Strings.String +From Stdlib Require Import String Fiat.ADTRefinement.GeneralBuildADTTactics Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples Fiat.QueryStructure.Specification.Representation.QueryStructureNotations diff --git a/src/QueryStructure/Automation/SearchTerms/InclusionSearchTerms.v b/src/QueryStructure/Automation/SearchTerms/InclusionSearchTerms.v index fc846b738..9b0868aef 100644 --- a/src/QueryStructure/Automation/SearchTerms/InclusionSearchTerms.v +++ b/src/QueryStructure/Automation/SearchTerms/InclusionSearchTerms.v @@ -1,5 +1,5 @@ Require Import - Coq.Strings.String + Stdlib.Strings.String Fiat.Common.String_as_OT Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.SearchTerms.ListInclusion diff --git a/src/QueryStructure/Implementation/Constraints/ConstraintChecksRefinements.v b/src/QueryStructure/Implementation/Constraints/ConstraintChecksRefinements.v index 3a41df4ff..b4f907480 100644 --- a/src/QueryStructure/Implementation/Constraints/ConstraintChecksRefinements.v +++ b/src/QueryStructure/Implementation/Constraints/ConstraintChecksRefinements.v @@ -1,10 +1,10 @@ Require Export Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.Operations.Query. -Require Import Coq.Lists.List +Require Import Stdlib.Lists.List Coq.Arith.Compare_dec Coq.Bool.Bool - Coq.Strings.String + Stdlib.Strings.String Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms diff --git a/src/QueryStructure/Implementation/Constraints/ConstraintChecksUnfoldings.v b/src/QueryStructure/Implementation/Constraints/ConstraintChecksUnfoldings.v index eadd9baec..a37dcf262 100644 --- a/src/QueryStructure/Implementation/Constraints/ConstraintChecksUnfoldings.v +++ b/src/QueryStructure/Implementation/Constraints/ConstraintChecksUnfoldings.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Coq.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith +Require Import Stdlib.Lists.List Stdlib.Strings.String Stdlib.Sets.Ensembles Stdlib.Arith.Arith Fiat.Common.ilist Fiat.Common.StringBound Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.QueryStructure.Specification.Representation.QueryStructureSchema diff --git a/src/QueryStructure/Implementation/DataStructures/BagADT/BagADT.v b/src/QueryStructure/Implementation/DataStructures/BagADT/BagADT.v index 5435bd1e6..c8733466e 100644 --- a/src/QueryStructure/Implementation/DataStructures/BagADT/BagADT.v +++ b/src/QueryStructure/Implementation/DataStructures/BagADT/BagADT.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String +From Stdlib Require Import String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality diff --git a/src/QueryStructure/Implementation/DataStructures/BagADT/BagImplementation.v b/src/QueryStructure/Implementation/DataStructures/BagADT/BagImplementation.v index 6e49b68fc..8553ae53a 100644 --- a/src/QueryStructure/Implementation/DataStructures/BagADT/BagImplementation.v +++ b/src/QueryStructure/Implementation/DataStructures/BagADT/BagImplementation.v @@ -7,7 +7,7 @@ Require Export Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist. -Require Import Coq.Bool.Bool Coq.Strings.String +Require Import Stdlib.Bool.Bool Stdlib.Strings.String Coq.Arith.Arith Coq.Structures.OrderedTypeEx Fiat.Common.String_as_OT Fiat.Common.i2list diff --git a/src/QueryStructure/Implementation/DataStructures/BagADT/IndexSearchTerms.v b/src/QueryStructure/Implementation/DataStructures/BagADT/IndexSearchTerms.v index c16c57d68..c91a0f9f9 100644 --- a/src/QueryStructure/Implementation/DataStructures/BagADT/IndexSearchTerms.v +++ b/src/QueryStructure/Implementation/DataStructures/BagADT/IndexSearchTerms.v @@ -2,7 +2,7 @@ Require Import Coq.Lists.List Coq.Program.Program Coq.Bool.Bool - Coq.Strings.String + Stdlib.Strings.String Fiat.Common.ilist Fiat.Common.ilist2 Fiat.Common.ilist3 diff --git a/src/QueryStructure/Implementation/DataStructures/BagADT/QueryStructureImplementation.v b/src/QueryStructure/Implementation/DataStructures/BagADT/QueryStructureImplementation.v index 0318e1b1e..72690d417 100644 --- a/src/QueryStructure/Implementation/DataStructures/BagADT/QueryStructureImplementation.v +++ b/src/QueryStructure/Implementation/DataStructures/BagADT/QueryStructureImplementation.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List Coq.Program.Program - Coq.Bool.Bool Coq.Strings.String +Require Import Stdlib.Lists.List Stdlib.Program.Program + Coq.Bool.Bool Stdlib.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.ilist3 Fiat.Common.i3list diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/BagsInterface.v b/src/QueryStructure/Implementation/DataStructures/Bags/BagsInterface.v index e0d605c4a..fcd4a7446 100644 --- a/src/QueryStructure/Implementation/DataStructures/Bags/BagsInterface.v +++ b/src/QueryStructure/Implementation/DataStructures/Bags/BagsInterface.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Export Coq.Program.Program Coq.Sorting.Permutation. +Require Export Stdlib.Program.Program Stdlib.Sorting.Permutation. Unset Implicit Arguments. Global Set Asymmetric Patterns. diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/BagsOfTuples.v b/src/QueryStructure/Implementation/DataStructures/Bags/BagsOfTuples.v index 95ef83744..f0c392455 100644 --- a/src/QueryStructure/Implementation/DataStructures/Bags/BagsOfTuples.v +++ b/src/QueryStructure/Implementation/DataStructures/Bags/BagsOfTuples.v @@ -6,7 +6,7 @@ Require Export Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterf Fiat.QueryStructure.Specification.Representation.Heading Coq.Lists.List Coq.Program.Program Fiat.Common.ilist. -Require Import Coq.Bool.Bool Coq.Strings.String +Require Import Stdlib.Bool.Bool Stdlib.Strings.String Coq.Structures.OrderedTypeEx Coq.NArith.BinNat Coq.ZArith.ZArith_dec Coq.Arith.Arith Coq.FSets.FMapAVL diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/BagsProperties.v b/src/QueryStructure/Implementation/DataStructures/Bags/BagsProperties.v index 909a28a83..47d292633 100644 --- a/src/QueryStructure/Implementation/DataStructures/Bags/BagsProperties.v +++ b/src/QueryStructure/Implementation/DataStructures/Bags/BagsProperties.v @@ -1,4 +1,4 @@ -Require Import Coq.Arith.Arith +Require Import Stdlib.Arith.Arith Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms. diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/BagsTactics.v b/src/QueryStructure/Implementation/DataStructures/Bags/BagsTactics.v index bd6a12ed2..2b95c9330 100644 --- a/src/QueryStructure/Implementation/DataStructures/Bags/BagsTactics.v +++ b/src/QueryStructure/Implementation/DataStructures/Bags/BagsTactics.v @@ -1,5 +1,5 @@ -Require Import Coq.Strings.String Coq.Arith.Arith - Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface +From Stdlib Require Import String Arith. +Require Import Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.ListImplementation diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/CachingBags.v b/src/QueryStructure/Implementation/DataStructures/Bags/CachingBags.v index 4a7d8ebee..6cdd900c7 100644 --- a/src/QueryStructure/Implementation/DataStructures/Bags/CachingBags.v +++ b/src/QueryStructure/Implementation/DataStructures/Bags/CachingBags.v @@ -1,4 +1,4 @@ -Require Export Coq.Lists.List Coq.Program.Program +Require Export Stdlib.Lists.List Stdlib.Program.Program Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties. Require Import Fiat.Common.List.ListFacts. diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/CountingListBags.v b/src/QueryStructure/Implementation/DataStructures/Bags/CountingListBags.v index 2f65d8eed..2bf2fc98d 100644 --- a/src/QueryStructure/Implementation/DataStructures/Bags/CountingListBags.v +++ b/src/QueryStructure/Implementation/DataStructures/Bags/CountingListBags.v @@ -1,7 +1,7 @@ Require Export Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface. Unset Implicit Arguments. -Require Import Coq.Arith.Arith +Require Import Stdlib.Arith.Arith Fiat.Common.List.ListFacts. Open Scope list_scope. diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/ListBags.v b/src/QueryStructure/Implementation/DataStructures/Bags/ListBags.v index 44654cd65..bb334b93b 100644 --- a/src/QueryStructure/Implementation/DataStructures/Bags/ListBags.v +++ b/src/QueryStructure/Implementation/DataStructures/Bags/ListBags.v @@ -63,7 +63,7 @@ Section ListBags. firstorder. Qed. - Require Import Coq.ZArith.ZArith. + From Stdlib Require Import ZArith. Lemma List_BagCountCorrect_aux : forall (container: list TItem) (search_term: TSearchTerm) default, length (List.filter (bfind_matcher search_term) container) + default = diff --git a/src/QueryStructure/Implementation/DataStructures/Bags/NatCompare_Facts.v b/src/QueryStructure/Implementation/DataStructures/Bags/NatCompare_Facts.v index b4a77bdf1..8ab7f3df9 100644 --- a/src/QueryStructure/Implementation/DataStructures/Bags/NatCompare_Facts.v +++ b/src/QueryStructure/Implementation/DataStructures/Bags/NatCompare_Facts.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +From Stdlib Require Import ZArith. Require Export Fiat.Common.Coq__8_4__8_5__Compat. #[global] diff --git a/src/QueryStructure/Implementation/Operations/BagADT/Refinements.v b/src/QueryStructure/Implementation/Operations/BagADT/Refinements.v index cfc989fc2..39c1a7b5b 100644 --- a/src/QueryStructure/Implementation/Operations/BagADT/Refinements.v +++ b/src/QueryStructure/Implementation/Operations/BagADT/Refinements.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Export Coq.Lists.List Coq.Program.Program +Require Export Stdlib.Lists.List Stdlib.Program.Program Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist2 @@ -7,8 +7,8 @@ Require Export Coq.Lists.List Coq.Program.Program Fiat.Common.ilist3 Fiat.Common.i3list. -Require Import Coq.Bool.Bool - Coq.Strings.String +Require Import Stdlib.Bool.Bool + Stdlib.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.String_as_OT diff --git a/src/QueryStructure/Implementation/Operations/General/DeleteRefinements.v b/src/QueryStructure/Implementation/Operations/General/DeleteRefinements.v index e39095eb2..4316ab5b4 100644 --- a/src/QueryStructure/Implementation/Operations/General/DeleteRefinements.v +++ b/src/QueryStructure/Implementation/Operations/General/DeleteRefinements.v @@ -1,5 +1,5 @@ -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles - Fiat.Common.List.ListFacts +From Stdlib Require Import String ZArith List FunctionalExtensionality Ensembles. +Require Import Fiat.Common.List.ListFacts Fiat.Computation Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.ADT diff --git a/src/QueryStructure/Implementation/Operations/General/EmptyRefinements.v b/src/QueryStructure/Implementation/Operations/General/EmptyRefinements.v index 15a2ebb7e..fecb356e2 100644 --- a/src/QueryStructure/Implementation/Operations/General/EmptyRefinements.v +++ b/src/QueryStructure/Implementation/Operations/General/EmptyRefinements.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String +From Stdlib Require Import String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality diff --git a/src/QueryStructure/Implementation/Operations/General/InsertRefinements.v b/src/QueryStructure/Implementation/Operations/General/InsertRefinements.v index eade4097e..297bffcfb 100644 --- a/src/QueryStructure/Implementation/Operations/General/InsertRefinements.v +++ b/src/QueryStructure/Implementation/Operations/General/InsertRefinements.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List +From Stdlib Require Import String ZArith List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Computation Fiat.Computation.Refinements.Iterate_Decide_Comp diff --git a/src/QueryStructure/Implementation/Operations/General/MutateRefinements.v b/src/QueryStructure/Implementation/Operations/General/MutateRefinements.v index be13f0774..35bda4890 100644 --- a/src/QueryStructure/Implementation/Operations/General/MutateRefinements.v +++ b/src/QueryStructure/Implementation/Operations/General/MutateRefinements.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String +From Stdlib Require Import String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality diff --git a/src/QueryStructure/Implementation/Operations/General/QueryRefinements.v b/src/QueryStructure/Implementation/Operations/General/QueryRefinements.v index 5bda80528..171e4343b 100644 --- a/src/QueryStructure/Implementation/Operations/General/QueryRefinements.v +++ b/src/QueryStructure/Implementation/Operations/General/QueryRefinements.v @@ -3,7 +3,7 @@ Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.ZArith.ZArith - Coq.Strings.String + Stdlib.Strings.String Coq.Lists.List Coq.Sorting.Permutation Coq.Bool.Bool diff --git a/src/QueryStructure/Implementation/Operations/General/QueryStructureRefinements.v b/src/QueryStructure/Implementation/Operations/General/QueryStructureRefinements.v index 9bba66fa0..a37d78286 100644 --- a/src/QueryStructure/Implementation/Operations/General/QueryStructureRefinements.v +++ b/src/QueryStructure/Implementation/Operations/General/QueryStructureRefinements.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String +From Stdlib Require Import String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality diff --git a/src/QueryStructure/Implementation/Operations/List/ListInsertRefinements.v b/src/QueryStructure/Implementation/Operations/List/ListInsertRefinements.v index 589fd759d..082d8ff45 100644 --- a/src/QueryStructure/Implementation/Operations/List/ListInsertRefinements.v +++ b/src/QueryStructure/Implementation/Operations/List/ListInsertRefinements.v @@ -1,5 +1,5 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat. -Require Import Coq.Strings.String +From Stdlib Require Import String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality diff --git a/src/QueryStructure/Implementation/Operations/List/ListQueryRefinements.v b/src/QueryStructure/Implementation/Operations/List/ListQueryRefinements.v index 0c9f5c19d..a19fb38e3 100644 --- a/src/QueryStructure/Implementation/Operations/List/ListQueryRefinements.v +++ b/src/QueryStructure/Implementation/Operations/List/ListQueryRefinements.v @@ -1,4 +1,4 @@ -Require Import Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List +From Stdlib Require Import String ZArith List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Computation diff --git a/src/QueryStructure/Specification/Constraints/tupleAgree.v b/src/QueryStructure/Specification/Constraints/tupleAgree.v index 3bbdb5d65..796acd578 100644 --- a/src/QueryStructure/Specification/Constraints/tupleAgree.v +++ b/src/QueryStructure/Specification/Constraints/tupleAgree.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List +Require Import Stdlib.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple diff --git a/src/QueryStructure/Specification/Operations/Delete.v b/src/QueryStructure/Specification/Operations/Delete.v index 949ca1634..866752b7b 100644 --- a/src/QueryStructure/Specification/Operations/Delete.v +++ b/src/QueryStructure/Specification/Operations/Delete.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Computation.Core diff --git a/src/QueryStructure/Specification/Operations/Empty.v b/src/QueryStructure/Specification/Operations/Empty.v index 29186d012..d134c58f8 100644 --- a/src/QueryStructure/Specification/Operations/Empty.v +++ b/src/QueryStructure/Specification/Operations/Empty.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Common.StringBound diff --git a/src/QueryStructure/Specification/Operations/FlattenCompList.v b/src/QueryStructure/Specification/Operations/FlattenCompList.v index 66a659600..de02c317b 100644 --- a/src/QueryStructure/Specification/Operations/FlattenCompList.v +++ b/src/QueryStructure/Specification/Operations/FlattenCompList.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List +Require Import Stdlib.Lists.List Coq.Program.Program Coq.Sets.Ensembles. Require Import Fiat.Common diff --git a/src/QueryStructure/Specification/Operations/Insert.v b/src/QueryStructure/Specification/Operations/Insert.v index 3f08e93dc..877fd69c3 100644 --- a/src/QueryStructure/Specification/Operations/Insert.v +++ b/src/QueryStructure/Specification/Operations/Insert.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Computation.Core diff --git a/src/QueryStructure/Specification/Operations/InsertAll.v b/src/QueryStructure/Specification/Operations/InsertAll.v index 3cf2b50c1..1f0e32291 100644 --- a/src/QueryStructure/Specification/Operations/InsertAll.v +++ b/src/QueryStructure/Specification/Operations/InsertAll.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Computation.Core diff --git a/src/QueryStructure/Specification/Operations/Mutate.v b/src/QueryStructure/Specification/Operations/Mutate.v index b14031a5b..91e795dff 100644 --- a/src/QueryStructure/Specification/Operations/Mutate.v +++ b/src/QueryStructure/Specification/Operations/Mutate.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Computation.Core diff --git a/src/QueryStructure/Specification/Operations/Query.v b/src/QueryStructure/Specification/Operations/Query.v index c5a1568a0..28be0e545 100644 --- a/src/QueryStructure/Specification/Operations/Query.v +++ b/src/QueryStructure/Specification/Operations/Query.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Computation.Core @@ -108,7 +108,7 @@ Definition foldOption {A: Type} (f : A -> A -> A) seq := (* Specs for the min and the max of lists of values. *) -Require Import Coq.NArith.NArith Coq.ZArith.ZArith. +Require Import Stdlib.NArith.NArith Stdlib.ZArith.ZArith. Definition FoldAggregateOption {A} (updater: A -> A -> A) (rows: Comp (list A)) := l <- rows; diff --git a/src/QueryStructure/Specification/Operations/Update.v b/src/QueryStructure/Specification/Operations/Update.v index 33aa63c52..1a4cbaa45 100644 --- a/src/QueryStructure/Specification/Operations/Update.v +++ b/src/QueryStructure/Specification/Operations/Update.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Computation.Core diff --git a/src/QueryStructure/Specification/Representation/Heading.v b/src/QueryStructure/Specification/Representation/Heading.v index 1d1c1dc6e..c9468326f 100644 --- a/src/QueryStructure/Specification/Representation/Heading.v +++ b/src/QueryStructure/Specification/Representation/Heading.v @@ -2,7 +2,7 @@ Require Import Coq.Vectors.Vector Coq.Vectors.Vector Coq.Lists.List - Coq.Strings.String + Stdlib.Strings.String Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.ilist diff --git a/src/QueryStructure/Specification/Representation/Heading2.v b/src/QueryStructure/Specification/Representation/Heading2.v index 105c81cef..177cc2855 100644 --- a/src/QueryStructure/Specification/Representation/Heading2.v +++ b/src/QueryStructure/Specification/Representation/Heading2.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.List Coq.Strings.String Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles +Require Import Stdlib.Lists.List Stdlib.Strings.String Stdlib.Logic.FunctionalExtensionality Stdlib.Sets.Ensembles Fiat.Common.ilist Fiat.Common.StringBound Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Notations. diff --git a/src/QueryStructure/Specification/Representation/QueryStructure.v b/src/QueryStructure/Specification/Representation/QueryStructure.v index d40f88542..8ef3249e4 100644 --- a/src/QueryStructure/Specification/Representation/QueryStructure.v +++ b/src/QueryStructure/Specification/Representation/QueryStructure.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Arith.Arith diff --git a/src/QueryStructure/Specification/Representation/QueryStructureNotations.v b/src/QueryStructure/Specification/Representation/QueryStructureNotations.v index 858296025..e274356cc 100644 --- a/src/QueryStructure/Specification/Representation/QueryStructureNotations.v +++ b/src/QueryStructure/Specification/Representation/QueryStructureNotations.v @@ -1,4 +1,4 @@ -Require Export Coq.Strings.String +Require Export Stdlib.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality diff --git a/src/QueryStructure/Specification/Representation/QueryStructureSchema.v b/src/QueryStructure/Specification/Representation/QueryStructureSchema.v index 3cf7921b9..d1d2d1400 100644 --- a/src/QueryStructure/Specification/Representation/QueryStructureSchema.v +++ b/src/QueryStructure/Specification/Representation/QueryStructureSchema.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Fiat.Common Coq.Arith.Arith Coq.Logic.FunctionalExtensionality @@ -172,7 +172,7 @@ Instance Query_eq_list {A : Type} : Query_eq (list A) := {| A_eq_dec := list_eq_dec (@A_eq_dec A a_eq_dec) |}. -Require Import Coq.NArith.NArith Coq.ZArith.ZArith. +Require Import Stdlib.NArith.NArith Stdlib.ZArith.ZArith. #[global] Instance AN_eq : Query_eq N := {| A_eq_dec := N.eq_dec |}. #[global] diff --git a/src/QueryStructure/Specification/Representation/Relation.v b/src/QueryStructure/Specification/Representation/Relation.v index 5725bd097..b03fcf75f 100644 --- a/src/QueryStructure/Specification/Representation/Relation.v +++ b/src/QueryStructure/Specification/Representation/Relation.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.StringBound diff --git a/src/QueryStructure/Specification/Representation/Schema.v b/src/QueryStructure/Specification/Representation/Schema.v index 33a608af4..14da73d3d 100644 --- a/src/QueryStructure/Specification/Representation/Schema.v +++ b/src/QueryStructure/Specification/Representation/Schema.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.StringBound diff --git a/src/QueryStructure/Specification/Representation/Tuple.v b/src/QueryStructure/Specification/Representation/Tuple.v index 4973ccf09..df66dae5f 100644 --- a/src/QueryStructure/Specification/Representation/Tuple.v +++ b/src/QueryStructure/Specification/Representation/Tuple.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.ilist2 diff --git a/src/QueryStructure/Specification/Representation/Tuple2.v b/src/QueryStructure/Specification/Representation/Tuple2.v index 9d6489f6b..e74ee5f37 100644 --- a/src/QueryStructure/Specification/Representation/Tuple2.v +++ b/src/QueryStructure/Specification/Representation/Tuple2.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.ilist2 diff --git a/src/QueryStructure/Specification/Representation/TupleADT.v b/src/QueryStructure/Specification/Representation/TupleADT.v index 0200e6010..011135d49 100644 --- a/src/QueryStructure/Specification/Representation/TupleADT.v +++ b/src/QueryStructure/Specification/Representation/TupleADT.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Arith.Arith Coq.ZArith.ZArith Fiat.Common.ilist2 diff --git a/src/QueryStructure/Specification/Representation/TupleADT2.v b/src/QueryStructure/Specification/Representation/TupleADT2.v index d70283e06..c1e333deb 100644 --- a/src/QueryStructure/Specification/Representation/TupleADT2.v +++ b/src/QueryStructure/Specification/Representation/TupleADT2.v @@ -1,5 +1,5 @@ -Require Import Coq.Lists.List - Coq.Strings.String +Require Import Stdlib.Lists.List + Stdlib.Strings.String Coq.Arith.Arith Coq.ZArith.ZArith Fiat.Common.ilist2 diff --git a/src/QueryStructure/Specification/SearchTerms/InRange.v b/src/QueryStructure/Specification/SearchTerms/InRange.v index d8cf7a115..940e37b23 100644 --- a/src/QueryStructure/Specification/SearchTerms/InRange.v +++ b/src/QueryStructure/Specification/SearchTerms/InRange.v @@ -1,4 +1,4 @@ -Require Import Coq.Arith.Compare_dec +Require Import Stdlib.Arith.Compare_dec Coq.ZArith.ZArith Fiat.QueryStructure.Specification.Representation.QueryStructureNotations.