aboutsummaryrefslogtreecommitdiff
path: root/src/Assembly
diff options
context:
space:
mode:
authorGravatar Robert Sloan <varomodt@google.com>2016-10-14 15:58:27 -0700
committerGravatar Robert Sloan <varomodt@google.com>2016-10-14 15:58:27 -0700
commit9aaac03f6c5be0f804ed1d996d52fcefb1e57944 (patch)
tree73e954502dad1ec8b21b55a15e123b2d0bca75c0 /src/Assembly
parentad5c28e00ca3fb89508138354ddaf2f5ba79bd0b (diff)
Use 64-bit limbs in Pipelines
Diffstat (limited to 'src/Assembly')
-rw-r--r--src/Assembly/GF25519.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v
index 081ddc008..84e692424 100644
--- a/src/Assembly/GF25519.v
+++ b/src/Assembly/GF25519.v
@@ -6,8 +6,8 @@ Require Import Crypto.Specific.GF25519.
Require Import Crypto.Util.Tuple.
Module GF25519.
- Definition bits: nat := 32.
- Definition width: Width bits := W32.
+ Definition bits: nat := 64.
+ Definition width: Width bits := W64.
Fixpoint makeBoundList {n} k (b: @WordRangeOpt n) :=
match k with