diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-14 23:22:39 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-14 23:22:39 -0400 |
| commit | d626e82b7286d44f41ef5e03a201573f019bbd8b (patch) | |
| tree | 16150b557d9cb61db81584de62cabae1ed58c947 /src | |
| parent | 15dcfc57b19890f20e5bca7c1032ec75031a7f75 (diff) | |
Prelinearize so we can simplify more arithmetic in pipeline
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Definition.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v index 2d7b3f15b..1592975b8 100644 --- a/src/Compilers/Z/Bounds/Pipeline/Definition.v +++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v @@ -34,7 +34,7 @@ Require Import Crypto.Compilers.Z.ArithmeticSimplifierInterp. (** *** Definition of the Pre-Wf Pipeline *) (** Do not change the name or the type of this definition *) Definition PreWfPipeline {t} (e : Expr base_type op t) : Expr base_type op _ - := ExprEta (SimplifyArith e). + := ExprEta (SimplifyArith (Linearize e)). (** *** Correctness proof of the Pre-Wf Pipeline *) (** Do not change the statement of this lemma. You shouldn't need to |