12 files changed, 20 insertions, 1 deletions
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 <https://tools.ietf.org/html/rfc7748#section-5.2>,
    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.