aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
diff options
context:
space:
mode:
Diffstat (limited to 'src/Specific')
-rw-r--r--src/Specific/FancyMachine256/Core.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v
index 900ac92a9..adb29e81f 100644
--- a/src/Specific/FancyMachine256/Core.v
+++ b/src/Specific/FancyMachine256/Core.v
@@ -8,6 +8,7 @@ Require Export Crypto.LegacyArithmetic.ArchitectureToZLike.
Require Export Crypto.LegacyArithmetic.ArchitectureToZLikeProofs.
Require Export Crypto.Util.Tuple.
Require Import Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod.
+Require Import Crypto.Compilers.Named.Context.
Require Export Crypto.Compilers.Named.Syntax.
Require Export Crypto.Compilers.Named.PositiveContext.
Require Import Crypto.Compilers.Named.DeadCodeElimination.