4 files changed, 6 insertions, 1 deletions
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.