aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jade Philipoom <jadep@mit.edu>2016-02-15 19:06:02 -0500
committerGravatar Robert Sloan <varomodt@gmail.com>2016-06-22 13:40:30 -0400
commitdbfdb9a409afdc0b749d45bdcc4c52cfecb3829f (patch)
tree201185db7b447885bff5dbab4d75d84e5049f746 /src
parent1a07a4a34a05b9a9dcabdd69c06e1618e76e80de (diff)
fixed renamed files and added imports for encodings
Diffstat (limited to 'src')
-rw-r--r--src/EdDSAProofs.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/EdDSAProofs.v b/src/EdDSAProofs.v
index da0ea5e8b..7357284e1 100644
--- a/src/EdDSAProofs.v
+++ b/src/EdDSAProofs.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Spec.EdDSA.
+Require Import Crypto.Spec.EdDSA Crypto.Spec.Encoding.
Require Import NPeano.
Require Import Bedrock.Word.
Require Import Znumtheory BinInt ZArith.
@@ -116,4 +116,4 @@ Section EdDSAProofs.
Proof.
unfold verify, sign, public; arith; try break_if; intuition.
Qed.
-End EdDSAProofs. \ No newline at end of file
+End EdDSAProofs.