From c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 6 Apr 2017 22:53:07 -0400 Subject: rename-everything --- src/Spec/EdDSA.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Spec/EdDSA.v') 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; -- cgit v1.2.3