aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-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.