diff options
| author |  jadep <jadep@mit.edu> | 2019-03-14 15:04:10 -0400 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2019-04-03 23:34:53 +0100 |
| commit | a189b8ad9943cec026ea2797789d8dc72a6d3336 (patch) | |
| tree | 727a7957ee921526a701a8a50fb91209b9ee2b56 /src/Arithmetic/FancyMontgomeryReduction.v | |
| parent | 9c5a967ababd80425fe3b09f17f502ed5f0d6a11 (diff) | |
remove extraneous module identifiers
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 |