1 files changed, 2 insertions, 2 deletions
diff --git a/src/Arithmetic/FancyMontgomeryReduction.v b/src/Arithmetic/FancyMontgomeryReduction.v
index 51b578bed..f69f7c1d4 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 seq].
+      cbv [Partition.partition seq].
       repeat match goal with
                | _ => progress rewrite ?eval1, ?eval2
                | _ => progress rewrite ?Z.zselect_correct, ?Z.add_modulo_correct
@@ -127,4 +127,4 @@ Module MontgomeryReduction.
       apply reduce_via_partial_in_range; omega.
     Qed.
   End MontRed'.
-End MontgomeryReduction.
-\ No newline at end of file
+End MontgomeryReduction.