diff options
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. |