From 64825ae187b354e4a6647105ce52544abdb6f4ae Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
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/Curves/Montgomery/Affine.v          | 1 +
 src/Curves/Montgomery/AffineInstances.v | 1 +
 src/Curves/Montgomery/AffineProofs.v    | 1 +
 src/Curves/Montgomery/XZ.v              | 4 +++-
 4 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'src/Curves')

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.
-- 
cgit v1.2.3