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