diff options
27 files changed, 70 insertions, 70 deletions
diff --git a/src/BaseSystem.v b/src/BaseSystem.v index f0e0db077..4e07c4564 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -1,7 +1,7 @@ -Require Import List. -Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. -Require Import ZArith.ZArith ZArith.Zdiv. -Require Import Omega NPeano Arith. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. +Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Local Open Scope Z. diff --git a/src/BoundedIterOp.v b/src/BoundedIterOp.v index fbdc823ad..bd4f7d66e 100644 --- a/src/BoundedIterOp.v +++ b/src/BoundedIterOp.v @@ -1,5 +1,5 @@ Require Import Crypto.Tactics.VerdiTactics. -Require Import BinNums NArith Nnat ZArith. +Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith. Definition testbit_rev p i bound := Pos.testbit_nat p (bound - i). diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 8ef1b95d4..3740f5a29 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -4,7 +4,7 @@ Require Import Crypto.ModularArithmetic.FField. Require Import Crypto.ModularArithmetic.FNsatz. Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Eqdep_dec. +Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. Section CompleteEdwardsCurveTheorems. diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v index 7c1e173ee..84c1289f6 100644 --- a/src/CompleteEdwardsCurve/DoubleAndAdd.v +++ b/src/CompleteEdwardsCurve/DoubleAndAdd.v @@ -1,7 +1,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.BoundedIterOp. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import BinNums NArith Nnat ZArith. +Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith. Section EdwardsDoubleAndAdd. Context {prm:TwistedEdwardsParams}. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index e4dc140e1..fea4a99b3 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,4 +1,4 @@ -Require Import BinInt Znumtheory VerdiTactics. +Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics. Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. diff --git a/src/EdDSAProofs.v b/src/EdDSAProofs.v index 7357284e1..83467bf6d 100644 --- a/src/EdDSAProofs.v +++ b/src/EdDSAProofs.v @@ -1,11 +1,11 @@ Require Import Crypto.Spec.EdDSA Crypto.Spec.Encoding. -Require Import NPeano. +Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Bedrock.Word. -Require Import Znumtheory BinInt ZArith. +Require Import Coq.ZArith.Znumtheory Coq.ZArith.BinInt Coq.ZArith.ZArith. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. -Require Import Util.ListUtil Util.CaseUtil Util.ZUtil. -Require Import VerdiTactics. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope nat_scope. Section EdDSAProofs. diff --git a/src/ModularArithmetic/FField.v b/src/ModularArithmetic/FField.v index ac2ef48b5..4f2b623e0 100644 --- a/src/ModularArithmetic/FField.v +++ b/src/ModularArithmetic/FField.v @@ -1,5 +1,5 @@ Require Export Crypto.Spec.ModularArithmetic. -Require Export Field. +Require Export Coq.setoid_ring.Field. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. diff --git a/src/ModularArithmetic/FNsatz.v b/src/ModularArithmetic/FNsatz.v index a0f34073d..221b8d799 100644 --- a/src/ModularArithmetic/FNsatz.v +++ b/src/ModularArithmetic/FNsatz.v @@ -1,6 +1,6 @@ Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Export Crypto.ModularArithmetic.FField. -Require Import Nsatz. +Require Import Coq.nsatz.Nsatz. Ltac FqAsIntegralDomain := lazymatch goal with [H:Znumtheory.prime ?q |- _ ] => diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index f39cc4176..ddb689547 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -1,11 +1,11 @@ Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.ModularArithmetic.Pre. -Require Import Eqdep_dec. -Require Import Tactics.VerdiTactics. -Require Import BinInt Zdiv Znumtheory NArith. (* import Zdiv before Znumtheory *) -Require Import Coq.Classes.Morphisms Setoid. -Require Export Ring_theory Field_theory Field_tac. +Require Import Coq.Logic.Eqdep_dec. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *) +Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. +Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. Section ModularArithmeticPreliminaries. Context {m:Z}. diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 8c22a8091..b2bea21cf 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -1,9 +1,9 @@ -Require Import Zpower ZArith. -Require Import List. +Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. +Require Import Coq.Lists.List. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.BaseSystem. -Require Import VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope Z_scope. Module Type PseudoMersenneBaseParams (Import B:BaseCoefs) (Import M:Modulus). diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index 3432488c4..2978fdd42 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -1,6 +1,6 @@ -Require Import BinInt BinNat BinNums Zdiv Znumtheory. -Require Import Eqdep_dec. -Require Import EqdepFacts. +Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.Numbers.BinNums Coq.ZArith.Zdiv Coq.ZArith.Znumtheory. +Require Import Coq.Logic.Eqdep_dec. +Require Import Coq.Logic.EqdepFacts. Require Import Crypto.Tactics.VerdiTactics. Lemma Z_mod_mod x m : x mod m = (x mod m) mod m. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 40af15dac..91ac63d26 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -1,13 +1,13 @@ -Require Export Spec.ModularArithmetic ModularArithmetic.ModularArithmeticTheorems. -Require Export Ring_theory Field_theory Field_tac. +Require Export Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.ModularArithmeticTheorems. +Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. -Require Import Nsatz. +Require Import Coq.nsatz.Nsatz. Require Import Crypto.ModularArithmetic.Pre. -Require Import Util.NumTheoryUtil. -Require Import Tactics.VerdiTactics. -Require Import Coq.Classes.Morphisms Setoid. -Require Import BinInt BinNat ZArith Znumtheory NArith. (* import Zdiv before Znumtheory *) -Require Import Eqdep_dec. +Require Import Crypto.Util.NumTheoryUtil. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. +Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *) +Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil. Existing Class prime. diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v index 425816f9e..d6c7fa4b8 100644 --- a/src/ModularArithmetic/Tutorial.v +++ b/src/ModularArithmetic/Tutorial.v @@ -1,5 +1,5 @@ -Require Import BinInt Zpower ZArith Znumtheory. -Require Import Spec.ModularArithmetic ModularArithmetic.PrimeFieldTheorems. +Require Import Coq.ZArith.BinInt Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems. (* Example for modular arithmetic with a concrete modulus in a section *) diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 23e201405..8dbfdf7b9 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -1,4 +1,4 @@ -Require BinInt Znumtheory. +Require Coq.ZArith.BinInt Coq.ZArith.Znumtheory. Require Crypto.CompleteEdwardsCurve.Pre. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index e16cc73f6..92c36b56c 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -1,14 +1,14 @@ -Require Import ZArith.ZArith Zpower ZArith Znumtheory. -Require Import NPeano NArith. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith. Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding. Require Import Crypto.Spec.EdDSA. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.WordUtil Crypto.Util.NumTheoryUtil. Require Import Bedrock.Word. -Require Import VerdiTactics. -Require Import Decidable. -Require Import Omega. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Coq.Logic.Decidable. +Require Import Coq.omega.Omega. Local Open Scope nat_scope. Definition q : Z := (2 ^ 255 - 19)%Z. diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 45950f6a1..6f57d7bec 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -4,8 +4,8 @@ Require Import Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.Util.WordUtil. Require Bedrock.Word. -Require Znumtheory BinInt. -Require NPeano. +Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt. +Require Coq.Numbers.Natural.Peano.NPeano. Coercion Word.wordToNat : Word.word >-> nat. diff --git a/src/Spec/Encoding.v b/src/Spec/Encoding.v index 7bef9295b..14cf9d9d9 100644 --- a/src/Spec/Encoding.v +++ b/src/Spec/Encoding.v @@ -1,8 +1,8 @@ -Require Import ZArith.ZArith Zpower ZArith. -Require Import NPeano. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. Require Import Bedrock.Word. -Require Import VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.WordUtil. diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index da6a62ada..76efe3d79 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -1,4 +1,4 @@ -Require Znumtheory BinNums. +Require Coq.ZArith.Znumtheory Coq.Numbers.BinNums. Require Crypto.ModularArithmetic.Pre. diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v index 2fec05863..4823ef28f 100644 --- a/src/Spec/PointEncoding.v +++ b/src/Spec/PointEncoding.v @@ -1,11 +1,11 @@ -Require Import ZArith.ZArith Zpower ZArith Znumtheory. -Require Import NPeano NArith. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith. Require Import Crypto.Spec.Encoding Crypto.Encoding.EncodingTheorems. Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil. Require Import Bedrock.Word. -Require Import VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope F_scope. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 516efd8b2..0d3923945 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -1,10 +1,10 @@ -Require Import ModularArithmetic.PrimeFieldTheorems. -Require Import BaseSystem ModularBaseSystem. -Require Import List Util.ListUtil. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.BaseSystem Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Coq.Lists.List Crypto.Util.ListUtil. Import ListNotations. -Require Import ZArith.ZArith Zpower ZArith Znumtheory. -Require Import QArith.QArith QArith.Qround. -Require Import VerdiTactics. +Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.QArith.QArith Coq.QArith.Qround. +Require Import Crypto.Tactics.VerdiTactics. Close Scope Q. Ltac twoIndices i j base := diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v index 35f207ffc..af04a1e49 100644 --- a/src/Util/CaseUtil.v +++ b/src/Util/CaseUtil.v @@ -1,4 +1,4 @@ -Require Import Arith. +Require Import Coq.Arith.Arith. Ltac case_max := match goal with [ |- context[max ?x ?y] ] => diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 4524f5cb9..016a4f7bd 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -1,5 +1,5 @@ Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. -Require Import NArith BinPosDef. +Require Import Coq.NArith.NArith Coq.PArith.BinPosDef. Local Open Scope equiv_scope. Generalizable All Variables. diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 783e3f527..1f9a62457 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1,7 +1,7 @@ -Require Import List. -Require Import Omega. -Require Import Arith.Peano_dec. -Require Import VerdiTactics. +Require Import Coq.Lists.List. +Require Import Coq.omega.Omega. +Require Import Coq.Arith.Peano_dec. +Require Import Crypto.Tactics.VerdiTactics. Ltac boring := simpl; intuition; diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 4ba6d0808..6a62d6c22 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,4 +1,4 @@ -Require Import NPeano Omega. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. Local Open Scope nat_scope. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 5acef8b75..10ce148b0 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -1,8 +1,8 @@ -Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv. -Require Import Omega NPeano Arith. +Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. +Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil. Require Import Coqprime.Zp. -Require Import VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope Z. (* TODO: move somewhere else for lemmas about Coqprime? *) diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 49de971ef..17d04c60a 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -1,5 +1,5 @@ -Require Import NPeano. -Require Import ZArith.ZArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Coq.ZArith.ZArith. Require Import Bedrock.Word. Local Open Scope nat_scope. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 2cfab2e90..db3d84b2d 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1,5 +1,5 @@ -Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv. -Require Import Omega NPeano Arith. +Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. +Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil. Local Open Scope Z. |