aboutsummaryrefslogtreecommitdiff
path: root/src/BoundsPipeline.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/BoundsPipeline.v')
-rw-r--r--src/BoundsPipeline.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v
index f0c161dc2..6c21d7c64 100644
--- a/src/BoundsPipeline.v
+++ b/src/BoundsPipeline.v
@@ -29,7 +29,7 @@ Require Crypto.CStringification.
Require Crypto.LanguageWf.
Require Crypto.UnderLetsProofs.
Require Crypto.MiscCompilerPassesProofs.
-Require Crypto.RewriterProofs.
+Require Crypto.RewriterAll.
Require Crypto.AbstractInterpretationWf.
Require Crypto.AbstractInterpretationProofs.
Require Import Crypto.Util.Notations.
@@ -39,7 +39,7 @@ Import
Crypto.LanguageWf
Crypto.UnderLetsProofs
Crypto.MiscCompilerPassesProofs
- Crypto.RewriterProofs
+ Crypto.RewriterAll
Crypto.AbstractInterpretationWf
Crypto.AbstractInterpretationProofs
Crypto.Language
@@ -53,7 +53,7 @@ Import
LanguageWf.Compilers
UnderLetsProofs.Compilers
MiscCompilerPassesProofs.Compilers
- RewriterProofs.Compilers
+ RewriterAll.Compilers
AbstractInterpretationWf.Compilers
AbstractInterpretationProofs.Compilers
Language.Compilers