diff options
Diffstat (limited to 'src/Arithmetic/FancyMontgomeryReduction.v')
| -rw-r--r-- | src/Arithmetic/FancyMontgomeryReduction.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Arithmetic/FancyMontgomeryReduction.v b/src/Arithmetic/FancyMontgomeryReduction.v index 258b2327e..51b578bed 100644 --- a/src/Arithmetic/FancyMontgomeryReduction.v +++ b/src/Arithmetic/FancyMontgomeryReduction.v @@ -91,7 +91,7 @@ Module MontgomeryReduction. autorewrite with widemul. rewrite Rows.add_partitions, Rows.add_div by (distr_length; apply wprops; omega). (* rewrite R_two_pow. *) - cbv [Partition.partition seq]. + cbv [partition seq]. repeat match goal with | _ => progress rewrite ?eval1, ?eval2 | _ => progress rewrite ?Z.zselect_correct, ?Z.add_modulo_correct |