aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/GF25519Reflective
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-11-03 11:48:22 -0400
committerGravatar Jason Gross <jgross@mit.edu>2016-11-03 11:48:22 -0400
commit690d35a9f418fd3cf03ec7c746e201ebaa2fc1a0 (patch)
tree654683ee26dee03fa30ac7f2ac805cc9a00d3298 /src/Specific/GF25519Reflective
parentd8c2ec0923704838f00fcbd22c57a48eb476c75c (diff)
Fix bounds that were reversed
Diffstat (limited to 'src/Specific/GF25519Reflective')
-rw-r--r--src/Specific/GF25519Reflective/Common.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index 8df44742e..f554d6708 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/Common.v
@@ -49,7 +49,7 @@ Local Ltac bounds_from_list ls :=
Local Ltac make_bounds ls :=
compute;
- let v := bounds_from_list ls in
+ let v := bounds_from_list (List.rev ls) in
let v := (eval compute in v) in
exact v.