diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-03-01 11:14:11 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | cffd104774accd30a76fb3a18d94936b680d96e1 (patch) | |
| tree | fcb486b60a32e52edab4e5a50d76fd6a3ec6a1bf /src | |
| parent | 83be64b2de78732f226a6566a30779ec9eac5ba5 (diff) | |
remove undeclared lines from Ed25519Extraction.v
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/Ed25519Extraction.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/Experiments/Ed25519Extraction.v b/src/Experiments/Ed25519Extraction.v index 8ec018c5f..23acecc08 100644 --- a/src/Experiments/Ed25519Extraction.v +++ b/src/Experiments/Ed25519Extraction.v @@ -268,8 +268,6 @@ Extraction Inline Ed25519.Erep Ed25519.SRep Ed25519.ZNWord Ed25519.WordNZ. Extraction Inline GF25519BoundedCommon.fe25519. Extraction Inline EdDSARepChange.sign EdDSARepChange.splitSecretPrngCurve. Extraction Inline Crypto.Util.IterAssocOp.iter_op Crypto.Util.IterAssocOp.test_and_op. -Extraction Inline PointEncoding.Kencode_point. -Extraction Inline ExtendedCoordinates.Extended.point ExtendedCoordinates.Extended.coordinates ExtendedCoordinates.Extended.to_twisted ExtendedCoordinates.Extended.from_twisted ExtendedCoordinates.Extended.add_coordinates ExtendedCoordinates.Extended.add ExtendedCoordinates.Extended.opp ExtendedCoordinates.Extended.zero. (* ExtendedCoordinates.Extended.zero could be precomputed *) Extraction Inline CompleteEdwardsCurve.E.coordinates CompleteEdwardsCurve.E.zero. Extraction Inline GF25519BoundedCommon.proj_word GF25519BoundedCommon.Build_bounded_word GF25519BoundedCommon.Build_bounded_word'. Extraction Inline GF25519BoundedCommon.app_wire_digits GF25519BoundedCommon.wire_digit_bounds_exp. @@ -291,5 +289,4 @@ Extract Constant Ed25519.SHA512 => Extraction Inline MxDH.ladderstep MxDH.montladder. -Extraction "src/Experiments/Ed25519_noimports.hs" Ed25519.sign (* Ed25519.verify *). Extraction "src/Experiments/X25519_noimports.hs" Crypto.Experiments.Ed25519.x25519. |