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