aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/Bounds
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Z/Bounds')
-rw-r--r--src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v6
-rw-r--r--src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v7
-rw-r--r--src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v9
-rw-r--r--src/Compilers/Z/Bounds/Relax.v3
4 files changed, 21 insertions, 4 deletions
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
index 45566839a..b23e0ff1b 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
@@ -8,9 +8,13 @@ Require Import Crypto.Compilers.Z.Bounds.Interpretation.
Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics.
Require Import Crypto.Compilers.SmartMap.
Require Import Crypto.Util.ZRange.CornersMonotoneBounds.
-Require Import Crypto.Util.ZUtil.
Require Import Crypto.Util.ZUtil.Stabilization.
Require Import Crypto.Util.ZUtil.MulSplit.
+Require Import Crypto.Util.ZUtil.Modulo.
+Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
+Require Import Crypto.Util.ZUtil.Morphisms.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.PointedProp.
Require Import Crypto.Util.Bool.
Require Import Crypto.Util.FixedWordSizesEquality.
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
index 1701b4688..7ffe0beb1 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
@@ -7,7 +7,12 @@ Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Z.Bounds.Interpretation.
Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics.
Require Import Crypto.Compilers.SmartMap.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Morphisms.
+Require Import Crypto.Util.ZUtil.Log2.
+Require Import Crypto.Util.ZUtil.Pow2.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Util.ZUtil.Tactics.PeelLe.
Require Import Crypto.Util.Bool.
Require Import Crypto.Util.FixedWordSizesEquality.
Require Import Crypto.Util.Option.
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
index 71f4b758b..6486b2e00 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
@@ -1,7 +1,14 @@
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Psatz.
Require Import Crypto.Compilers.Z.Bounds.Interpretation.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Hints.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Require Import Crypto.Util.ZUtil.ZSimplify.Core.
+Require Import Crypto.Util.ZUtil.Log2.
+Require Import Crypto.Util.ZUtil.Shift.
+Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Notations.
Require Import Crypto.Util.ZRange.Operations.
Require Import Crypto.Util.Bool.
Require Import Crypto.Util.FixedWordSizesEquality.
diff --git a/src/Compilers/Z/Bounds/Relax.v b/src/Compilers/Z/Bounds/Relax.v
index 328ea5f48..8178592ed 100644
--- a/src/Compilers/Z/Bounds/Relax.v
+++ b/src/Compilers/Z/Bounds/Relax.v
@@ -15,7 +15,8 @@ Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.SplitInContext.
Require Import Crypto.Util.Option.
-Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.ZUtil.Log2.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.Bool.
Local Lemma helper logsz v