diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-16 14:02:06 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-16 14:02:06 -0700 |
| commit | 314fa69fe5512d3b23f160b87f412d537e061903 (patch) | |
| tree | 6370dc79bda8cd2024f24cba489a5b36eb9d5338 /src/Specific/FancyMachine256/Core.v | |
| parent | 7df948ed3b6799f3f59df04758ab779a53151aa1 (diff) | |
Split off lemmas about [InlineConst]
Diffstat (limited to 'src/Specific/FancyMachine256/Core.v')
| -rw-r--r-- | src/Specific/FancyMachine256/Core.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v index d11cfe6ad..19f04fd89 100644 --- a/src/Specific/FancyMachine256/Core.v +++ b/src/Specific/FancyMachine256/Core.v @@ -8,6 +8,7 @@ Require Export Crypto.Util.Tuple. Require Import Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod. Require Export Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Linearize. +Require Import Crypto.Reflection.Inline. Require Import Crypto.Reflection.CommonSubexpressionElimination. Require Export Crypto.Reflection.Reify. Require Export Crypto.Util.ZUtil. |