aboutsummaryrefslogtreecommitdiff
path: root/src/SpecificGen/GF25519_32Reflective
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-11-21 14:35:19 -0500
committerGravatar Jason Gross <jgross@mit.edu>2016-11-21 14:35:19 -0500
commitfb1000a384f041a96d45bf61d3b471435cf45fb5 (patch)
tree0fb0ec1f265c82869e434aea03676aa47776bd88 /src/SpecificGen/GF25519_32Reflective
parente24ef0e681761645fd93419b47c950adfb90e5a9 (diff)
Fix missing import for List.repeat in 8.4
Diffstat (limited to 'src/SpecificGen/GF25519_32Reflective')
-rw-r--r--src/SpecificGen/GF25519_32Reflective/Common.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v
index e5b147098..4801c64fd 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common.v
@@ -16,6 +16,7 @@ Require Import Crypto.Reflection.MapInterpWf.
Require Import Crypto.Reflection.WfReflective.
Require Import Crypto.Util.Tower.
Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.ListUtil.
Require Import Crypto.Util.ZUtil.
Require Import Crypto.Util.Tactics.
Require Import Crypto.Util.Notations.