diff options
| author |  Jason Gross <jagro@google.com> | 2018-06-28 13:34:23 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-06-28 13:34:23 -0400 |
| commit | 1c17c2de3e18aaab050061a082e98a31dfa6c585 (patch) | |
| tree | fe099691da5e3fb3c624d90443517328d83fee0d /src/Experiments/NewPipeline | |
| parent | b9d795f30a86ac7b203a185b4fce12a192befa6d (diff) | |
Remove useless Requires
Diffstat (limited to 'src/Experiments/NewPipeline')
| -rw-r--r-- | src/Experiments/NewPipeline/Arithmetic.v | 3 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Language.v | 1 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Rewriter.v | 3 |
3 files changed, 0 insertions, 7 deletions
diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index 44834e5e3..d263ca151 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -10,8 +10,6 @@ Require Import Crypto.Arithmetic.BarrettReduction.Generalized. Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZRange. -Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.Tactics.RunTacticAsConstr. Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Option. @@ -37,7 +35,6 @@ Require Import Crypto.Util.ZUtil Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. Require Import Crypto.Util.ZUtil.Hints.PullPush. Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Tactics.DebugPrint. Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.Equality. Import ListNotations. Local Open Scope Z_scope. diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v index a27936fef..0f67d73ec 100644 --- a/src/Experiments/NewPipeline/Language.v +++ b/src/Experiments/NewPipeline/Language.v @@ -6,7 +6,6 @@ Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. Require Import Crypto.Util.Option. Require Import Crypto.Util.ZRange. -Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.CPSNotations. diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v index aecf401d8..eecf89832 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Experiments/NewPipeline/Rewriter.v @@ -1,10 +1,7 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.ListUtil.FoldBool. -Require Import Crypto.Util.ZRange. -Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.Option. Require Import Crypto.Util.OptionList. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.CPSNotations. Require Crypto.Util.PrimitiveProd. Require Crypto.Util.PrimitiveHList. |