diff options
Diffstat (limited to 'src/CompleteEdwardsCurve')
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 2 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/DoubleAndAdd.v | 2 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 2 |
3 files changed, 3 insertions, 3 deletions
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. |