From 64825ae187b354e4a6647105ce52544abdb6f4ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Aug 2018 22:49:37 -0400 Subject: Import prim token notations before using them This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. c.f. https://github.com/coq/coq/pull/8064#issuecomment-415493362 Almost all changes were made via https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169#file-fix-py --- src/Algebra/Field_test.v | 1 + src/Compilers/ZExtended/MapBaseType.v | 1 + src/Curves/Montgomery/Affine.v | 1 + src/Curves/Montgomery/AffineInstances.v | 1 + src/Curves/Montgomery/AffineProofs.v | 1 + src/Curves/Montgomery/XZ.v | 4 +++- src/Experiments/NewPipeline/CLI.v | 1 + src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v | 1 + src/Spec/Ed25519.v | 2 ++ src/Spec/EdDSA.v | 1 + src/Spec/ModularArithmetic.v | 4 ++++ src/Spec/Test/X25519.v | 3 +++ 12 files changed, 20 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v index 3bdd65089..522010d5c 100644 --- a/src/Algebra/Field_test.v +++ b/src/Algebra/Field_test.v @@ -1,3 +1,4 @@ +Require Import Coq.PArith.BinPosDef. Require Import Crypto.Util.Decidable Crypto.Util.Notations. Require Import Crypto.Algebra.Ring Crypto.Algebra.Field. diff --git a/src/Compilers/ZExtended/MapBaseType.v b/src/Compilers/ZExtended/MapBaseType.v index 869017685..66b18f6f5 100644 --- a/src/Compilers/ZExtended/MapBaseType.v +++ b/src/Compilers/ZExtended/MapBaseType.v @@ -1,3 +1,4 @@ +Require Import Coq.ZArith.BinIntDef. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.Z.Syntax. diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v index 2e39c6b6c..dd3ae84cd 100644 --- a/src/Curves/Montgomery/Affine.v +++ b/src/Curves/Montgomery/Affine.v @@ -1,3 +1,4 @@ +Require Import Coq.PArith.BinPosDef. Require Import Crypto.Algebra.Field. Require Import Crypto.Util.GlobalSettings. Require Import Crypto.Util.Sum Crypto.Util.Prod. diff --git a/src/Curves/Montgomery/AffineInstances.v b/src/Curves/Montgomery/AffineInstances.v index 049a7695b..40bd15420 100644 --- a/src/Curves/Montgomery/AffineInstances.v +++ b/src/Curves/Montgomery/AffineInstances.v @@ -1,3 +1,4 @@ +Require Import Coq.PArith.BinPosDef. Require Import Crypto.Algebra.Field. Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine. Require Import Crypto.Spec.WeierstrassCurve Crypto.Curves.Weierstrass.Affine. diff --git a/src/Curves/Montgomery/AffineProofs.v b/src/Curves/Montgomery/AffineProofs.v index 588605c35..2de52c520 100644 --- a/src/Curves/Montgomery/AffineProofs.v +++ b/src/Curves/Montgomery/AffineProofs.v @@ -1,3 +1,4 @@ +Require Import Coq.PArith.BinPosDef. Require Import Crypto.Algebra.Field. Require Import Crypto.Util.GlobalSettings. Require Import Crypto.Util.Sum Crypto.Util.Prod. diff --git a/src/Curves/Montgomery/XZ.v b/src/Curves/Montgomery/XZ.v index c83dd4c2d..6b813ba04 100644 --- a/src/Curves/Montgomery/XZ.v +++ b/src/Curves/Montgomery/XZ.v @@ -1,3 +1,5 @@ +Require Import Coq.PArith.BinPosDef. +Require Import Coq.ZArith.BinIntDef. Require Import Crypto.Algebra.Field. Require Import Crypto.Util.GlobalSettings Crypto.Util.Notations. Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn. @@ -109,7 +111,7 @@ Module M. dlet z2 := tmp1l * tmp0l in ((x2, z2), (x3, z3))%core end. - + Context {cswap:bool->F->F->F*F}. Local Notation xor := Coq.Init.Datatypes.xorb. Local Open Scope core_scope. diff --git a/src/Experiments/NewPipeline/CLI.v b/src/Experiments/NewPipeline/CLI.v index 3d219049f..f82d9e2a6 100644 --- a/src/Experiments/NewPipeline/CLI.v +++ b/src/Experiments/NewPipeline/CLI.v @@ -1,4 +1,5 @@ Require Import Coq.ZArith.ZArith. +Require Import Coq.Strings.Ascii. Require Import Coq.Lists.List. Require Import Coq.Strings.String. Require Crypto.Util.Strings.String. diff --git a/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v b/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v index 00d41f23d..b2d76911c 100644 --- a/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v +++ b/src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.v @@ -1,4 +1,5 @@ Require Import Coq.ZArith.ZArith. +Require Import Coq.Strings.String. Require Import Coq.derive.Derive. Require Import Coq.Lists.List. Require Import Crypto.Experiments.NewPipeline.Arithmetic. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 914692508..e0fba6e23 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -1,4 +1,6 @@ Require Import Crypto.Spec.ModularArithmetic. +Require Import Coq.PArith.BinPosDef. +Require Import Coq.ZArith.BinIntDef. Require Import Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.Spec.EdDSA. diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 8518821fc..268925167 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -1,4 +1,5 @@ Require bbv.WordScope Crypto.Util.WordUtil. +Require Import Coq.ZArith.BinIntDef. Require Crypto.Algebra.Hierarchy Algebra.ScalarMult. Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt. Require Coq.Numbers.Natural.Peano.NPeano. diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v index 02c4dd742..567f3a004 100644 --- a/src/Spec/ModularArithmetic.v +++ b/src/Spec/ModularArithmetic.v @@ -1,3 +1,7 @@ +Require Import Coq.ZArith.BinIntDef. +Require Import Coq.NArith.BinNatDef. +Require Import Coq.PArith.BinPosDef. + Require Coq.ZArith.Znumtheory Coq.Numbers.BinNums. Require Crypto.Arithmetic.ModularArithmeticPre. diff --git a/src/Spec/Test/X25519.v b/src/Spec/Test/X25519.v index a4fed8dd4..97b3a5fe0 100644 --- a/src/Spec/Test/X25519.v +++ b/src/Spec/Test/X25519.v @@ -1,6 +1,9 @@ (* Test vectors from , with hex values converted to decimal using python like this: > int.from_bytes(binascii.unhexlify('deadbeef'), 'little') *) +Require Import Coq.NArith.BinNatDef. +Require Import Coq.ZArith.BinIntDef. +Require Import Coq.PArith.BinPosDef. Require Import Spec.ModularArithmetic Spec.MxDH Crypto.Util.Decidable. Definition F := F (2^255 - 19). Definition a : F := F.of_Z _ 486662. -- cgit v1.2.3