diff options
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; |