diff options
| author |  jadep <jade.philipoom@gmail.com> | 2018-09-15 15:05:24 -0400 |
|---|---|---|
| committer | jadephilipoom <jade.philipoom@gmail.com> | 2018-09-17 21:34:36 -0400 |
| commit | 76b81e8645d1a05442c54af2b76ff525e5c8c0f0 (patch) | |
| tree | db330819f67e2bb31d034c11e5c5963d441d2930 /src | |
| parent | 61f6a2d25c657372022395c9fce329e6bc11c409 (diff) | |
Change naming for partition
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 4da5a42de..8dd20fd85 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -3492,7 +3492,7 @@ Module BarrettReduction. Lemma partition_represents x : 0 <= x < 2^k*2^k -> - represents (Rows.partition w 2 x) x. + represents (Partition.partition w 2 x) x. Proof. intros; cbn. change_weight. Z.rewrite_mod_small. @@ -3897,7 +3897,7 @@ Module MontgomeryReduction. autorewrite with widemul. rewrite Rows.add_partitions, Rows.add_div by (distr_length; apply wprops; omega). rewrite R_two_pow. - cbv [Rows.partition seq]. rewrite !eval2. + cbv [Partition.partition seq]. rewrite !eval2. autorewrite with push_nth_default push_map. autorewrite with to_div_mod. rewrite ?Z.zselect_correct, ?Z.add_modulo_correct. change_weight. |