aboutsummaryrefslogtreecommitdiff
path: root/src/PushButtonSynthesis/UnsaturatedSolinas.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/PushButtonSynthesis/UnsaturatedSolinas.v')
-rw-r--r--src/PushButtonSynthesis/UnsaturatedSolinas.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v
index 509f5cdad..3dfb6bfca 100644
--- a/src/PushButtonSynthesis/UnsaturatedSolinas.v
+++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v
@@ -25,6 +25,9 @@ Require Import Crypto.Language.
Require Import Crypto.AbstractInterpretation.
Require Import Crypto.CStringification.
Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.ModOps.
+Require Import Crypto.Arithmetic.Partition.
+Require Import Crypto.Arithmetic.Freeze.
Require Import Crypto.BoundsPipeline.
Require Import Crypto.COperationSpecifications.
Require Import Crypto.PushButtonSynthesis.ReificationCache.