diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
| commit | c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 (patch) | |
| tree | db7187f6984acff324ca468e7b33d9285806a1eb /src/Spec/EdDSA.v | |
| parent | 21198245dab432d3c0ba2bb8a02254e7d0594382 (diff) | |
rename-everything
Diffstat (limited to 'src/Spec/EdDSA.v')
| -rw-r--r-- | src/Spec/EdDSA.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 67a1014f6..82a9ba6cc 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -1,7 +1,7 @@ Require Bedrock.Word Crypto.Util.WordUtil. Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt. Require Coq.Numbers.Natural.Peano.NPeano. -Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. +Require Crypto.Algebra.ScalarMult. Require Import Omega. (* TODO: remove this import when we drop 8.4 *) @@ -41,7 +41,7 @@ Section EdDSA. {Senc : F l -> Word.word b} (* normative encoding of scalars *) := { - EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp; + EdDSA_group:@Algebra.Hierarchy.group E Eeq Eadd Ezero Eopp; EdDSA_scalarmult:@Algebra.ScalarMult.is_scalarmult E Eeq Eadd Ezero EscalarMult; EdDSA_c_valid : c = 2 \/ c = 3; |