aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
diff options
context:
space:
mode:
Diffstat (limited to 'src/Specific')
-rw-r--r--src/Specific/GF25519Reflective/Common.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index aa9b88122..20e19392a 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/Common.v
@@ -5,6 +5,7 @@ Require Import Crypto.Specific.GF25519BoundedCommon.
Require Import Crypto.Reflection.Reify.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Z.Interpretations.
+Require Crypto.Reflection.Z.Interpretations.Relations.
Require Import Crypto.Reflection.Z.Reify.
Require Export Crypto.Reflection.Z.Syntax.
Require Import Crypto.Reflection.InterpWfRel.