remove extraneous module identifiers

7 files changed, 85 insertions, 84 deletions

diff --git a/src/Arithmetic/BarrettReduction.v b/src/Arithmetic/BarrettReduction.v
index b679a168c..2f1f272ac 100644
--- a/src/Arithmetic/BarrettReduction.v
+++ b/src/Arithmetic/BarrettReduction.v
@@ -61,7 +61,7 @@ Section Generic.
   Local Lemma M_pos : 0 < M.
   Proof. assert (0 <= b ^ (k - 1)) by Z.zero_bounds. lia. Qed.
   Local Lemma M_upper : M < weight n.
-  Proof. rewrite UniformWeight.uweight_eq_alt'. lia. Qed.
+  Proof. rewrite uweight_eq_alt'. lia. Qed.
   Local Lemma x_upper : x < b ^ (2 * k).
   Proof.
     assert (0 < b ^ k) by Z.zero_bounds.
@@ -115,15 +115,15 @@ Module Fancy.
             (k_pos : 0 < k) (* this can be inferred from other arguments but is easier to put here for tactics *)
             (k_eq : k = width * Z.of_nat sz).
     (* sz = 1, width = k = 256 *)
-    Local Notation w := (UniformWeight.uweight width). Local Notation eval := (Positional.eval w).
+    Local Notation w := (uweight width). Local Notation eval := (Positional.eval w).
     Context (mut Mt : list Z) (mut_correct : mut = partition w (sz+1) mu) (Mt_correct : Mt = partition w sz M).
     Context (mu_eq : mu = 2 ^ (2 * k) / M) (muHigh_one : mu / w sz = 1) (M_range : 2^(k-1) < M < 2^k).
 
-    Local Lemma wprops : @weight_properties w. Proof. apply UniformWeight.uwprops; auto with lia. Qed.
+    Local Lemma wprops : @weight_properties w. Proof. apply uwprops; auto with lia. Qed.
     Local Hint Resolve wprops.
     Hint Rewrite mut_correct Mt_correct : pull_partition.
 
-    Lemma w_eq_2k : w sz = 2^k. Proof. rewrite UniformWeight.uweight_eq_alt' by auto. congruence. Qed.
+    Lemma w_eq_2k : w sz = 2^k. Proof. rewrite uweight_eq_alt' by auto. congruence. Qed.
     Lemma mu_range : 2^k <= mu < 2^(k+1).
     Proof.
       rewrite mu_eq. assert (0 < 2^(k-1)) by Z.zero_bounds.
@@ -140,7 +140,7 @@ Module Fancy.
     Proof.
       pose proof mu_range. assert (0 < 2^k) by auto with zarith.
       assert (2^(k+1) = 2 * w sz); [ | lia].
-      rewrite k_eq, UniformWeight.uweight_eq_alt'.
+      rewrite k_eq, uweight_eq_alt'.
       rewrite Z.pow_add_r, Z.pow_1_r by lia. lia.
     Qed.
     Lemma M_range' : 0 <= M < w sz. (* more convenient form, especially for mod_small *)
@@ -206,20 +206,20 @@ Module Fancy.
         cbv [shiftr']. induction m; intros; [ reflexivity | ].
         rewrite !partition_step, seq_snoc.
         autorewrite with distr_length natsimplify push_map push_nth_default.
-        rewrite IHm, Z.rshi_correct, UniformWeight.uweight_S by auto with zarith.
+        rewrite IHm, Z.rshi_correct, uweight_S by auto with zarith.
         rewrite <-Z.mod_pull_div by auto with zarith.
         destruct (Nat.eq_dec (S m) tn); [subst tn | ]; rewrite !nth_default_partition by omega.
         { rewrite nth_default_out_of_bounds by distr_length.
           autorewrite with zsimplify. Z.rewrite_mod_small.
           rewrite Z.div_div_comm by auto with zarith; reflexivity. }
         { repeat match goal with
-                 | _ => rewrite UniformWeight.uweight_pull_mod by auto with zarith
+                 | _ => rewrite uweight_pull_mod by auto with zarith
                  | _ => rewrite Z.mod_mod_small by auto with zarith
                  | _ => rewrite <-Znumtheory.Zmod_div_mod by (Z.zero_bounds; auto with zarith)
-                 | _ => rewrite UniformWeight.uweight_eq_alt with (n:=1%nat) by auto with zarith
+                 | _ => rewrite uweight_eq_alt with (n:=1%nat) by auto with zarith
                  | |- context [(t / w (S m)) mod 2^width * 2^width] =>
                    replace (t / w (S m)) with (t / w m / 2^width) by
-                       (rewrite UniformWeight.uweight_S, Z.div_div by auto with zarith; f_equal; lia);
+                       (rewrite uweight_S, Z.div_div by auto with zarith; f_equal; lia);
                      rewrite Z.mod_pull_div with (b:=2^width) by auto with zarith;
                      rewrite Z.mul_div_eq' by auto with zarith
                  | _ => progress autorewrite with natsimplify zsimplify_fast zsimplify
@@ -239,11 +239,11 @@ Module Fancy.
         pose proof (Z.mod_pos_bound n width ltac:(omega)).
         assert (t / 2 ^ (n - n mod width) < w (tn - Z.to_nat (n / width))).
         { apply Z.div_lt_upper_bound; [solve [Z.zero_bounds] | ].
-          rewrite UniformWeight.uweight_eq_alt' in *.
+          rewrite uweight_eq_alt' in *.
           rewrite <-Z.pow_add_r, Nat2Z.inj_sub, Z2Nat.id, <-Z.mul_div_eq by auto with zarith.
           autorewrite with push_Zmul zsimplify. auto with zarith. }
         repeat match goal with
-               | _ => progress rewrite ?UniformWeight.uweight_skipn_partition, ?UniformWeight.uweight_eq_alt' by auto with lia
+               | _ => progress rewrite ?uweight_skipn_partition, ?uweight_eq_alt' by auto with lia
                | _ => rewrite Z2Nat.id by Z.zero_bounds
                | _ => rewrite Z.mul_div_eq_full by auto with zarith
                | _ => rewrite shiftr'_correct by auto with zarith
@@ -267,16 +267,16 @@ Module Fancy.
       Qed.
 
       Lemma low_correct n a : (sz <= n)%nat -> low (partition w n a) = partition w sz a.
-      Proof. cbv [low]; auto using UniformWeight.uweight_firstn_partition with lia. Qed.
+      Proof. cbv [low]; auto using uweight_firstn_partition with lia. Qed.
       Lemma high_correct a : high (partition w (sz*2) a) = partition w sz (a / w sz).
-      Proof. cbv [high]. rewrite UniformWeight.uweight_skipn_partition by lia. f_equal; lia. Qed.
+      Proof. cbv [high]. rewrite uweight_skipn_partition by lia. f_equal; lia. Qed.
       Lemma fill_correct n m a :
         (n <= m)%nat ->
         fill m (partition w n a) = partition w m (a mod w n).
       Proof.
         cbv [fill]; intros. distr_length.
         rewrite <-partition_0 with (weight:=w).
-        rewrite UniformWeight.uweight_partition_app by lia.
+        rewrite uweight_partition_app by lia.
         f_equal; lia.
       Qed.
       Hint Rewrite low_correct high_correct fill_correct using lia : pull_partition.
@@ -335,7 +335,7 @@ Module Fancy.
         repeat match goal with
                | _ => progress autorewrite with pull_partition
                | _ => progress rewrite ?Ha, ?Ha0b1
-               | _ => rewrite UniformWeight.uweight_partition_app by lia;
+               | _ => rewrite uweight_partition_app by lia;
                         replace (sz+sz)%nat with (sz*2)%nat by lia
                | _ => rewrite Z.mod_pull_div by auto with zarith
                | _ => progress Z.rewrite_mod_small
@@ -343,8 +343,8 @@ Module Fancy.
                end.
       Qed.
 
-      Hint Rewrite UniformWeight.uweight_S UniformWeight.uweight_eq_alt' using lia : weight_to_pow.
-      Hint Rewrite <-UniformWeight.uweight_S UniformWeight.uweight_eq_alt' using lia : pow_to_weight.
+      Hint Rewrite uweight_S uweight_eq_alt' using lia : weight_to_pow.
+      Hint Rewrite <-uweight_S uweight_eq_alt' using lia : pow_to_weight.
 
       Lemma q1_range x :
         0 <= x < w (sz * 2) ->
@@ -416,7 +416,7 @@ Module Fancy.
         intros; cbv [cond_sub Let_In Z.cc_l]. autorewrite with pull_partition.
         rewrite nth_default_partition by lia.
         rewrite weight_0 by auto. autorewrite with zsimplify_fast.
-        rewrite UniformWeight.uweight_eq_alt' with (n:=1%nat). autorewrite with push_Zof_nat zsimplify.
+        rewrite uweight_eq_alt' with (n:=1%nat). autorewrite with push_Zof_nat zsimplify.
         rewrite <-Znumtheory.Zmod_div_mod by auto using Zpow_facts.Zpower_divide with zarith.
         rewrite Positional.select_eq with (n:=sz) by (distr_length; apply w).
         rewrite Rows.sub_partitions by (break_innermost_match; distr_length; auto).
@@ -452,7 +452,7 @@ Module Fancy.
       Lemma w_eq_22k : w (sz * 2) = 2 ^ (2 * k).
       Proof.
         replace (sz * 2)%nat with (sz + sz)%nat by lia.
-        rewrite UniformWeight.uweight_sum_indices, w_eq_2k, <-Z.pow_add_r by lia.
+        rewrite uweight_sum_indices, w_eq_2k, <-Z.pow_add_r by lia.
         f_equal; lia.
       Qed.
 
@@ -549,7 +549,7 @@ Module Fancy.
         partition w 2 (xLow + 2^k * xHigh) = [xLow;xHigh].
       Proof.
         replace k with width in M_range |- * by nia; intros. cbv [partition map seq].
-        rewrite !UniformWeight.uweight_S, !weight_0 by auto with zarith lia.
+        rewrite !uweight_S, !weight_0 by auto with zarith lia.
         autorewrite with zsimplify.
         rewrite <-Z.mod_pull_div by Z.zero_bounds.
         autorewrite with zsimplify. reflexivity.
@@ -568,7 +568,7 @@ Module Fancy.
         replace 2%nat with (sz*2)%nat by lia.
         rewrite fancy_reduce'_correct by nia.
         rewrite sz_eq_1; cbv [partition map seq hd].
-        rewrite !UniformWeight.uweight_S, !weight_0 by auto with zarith lia.
+        rewrite !uweight_S, !weight_0 by auto with zarith lia.
         autorewrite with zsimplify. reflexivity.
       Qed.
     End Def.
diff --git a/src/Arithmetic/BaseConversion.v b/src/Arithmetic/BaseConversion.v
index c06dd3d71..dde04ae2a 100644
--- a/src/Arithmetic/BaseConversion.v
+++ b/src/Arithmetic/BaseConversion.v
@@ -215,14 +215,14 @@ Module BaseConversion.
     Lemma widemul_correct a b :
       length a = m ->
       length b = m ->
-      widemul a b = Partition.partition sw nout (seval m a * seval m b). 
+      widemul a b = partition sw nout (seval m a * seval m b). 
     Proof. apply mul_converted_partitions; auto with zarith. Qed.
 
     Derive widemul_inlined
            SuchThat (forall a b,
                         length a = m ->
                         length b = m ->
-                        widemul_inlined a b = Partition.partition sw nout (seval m a * seval m b))
+                        widemul_inlined a b = partition sw nout (seval m a * seval m b))
            As widemul_inlined_correct.
     Proof.
       intros.
@@ -238,7 +238,7 @@ Module BaseConversion.
            SuchThat (forall a b,
                         length a = m ->
                         length b = m ->
-                        widemul_inlined_reverse a b = Partition.partition sw nout (seval m a * seval m b))
+                        widemul_inlined_reverse a b = partition sw nout (seval m a * seval m b))
            As widemul_inlined_reverse_correct.
     Proof.
       intros.
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
diff --git a/src/Arithmetic/Freeze.v b/src/Arithmetic/Freeze.v
index d59812dea..e766e7aea 100644
--- a/src/Arithmetic/Freeze.v
+++ b/src/Arithmetic/Freeze.v
@@ -3,6 +3,7 @@ Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil.
 Require Import Crypto.Arithmetic.BaseConversion.
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.ModOps.
+Require Import Crypto.Arithmetic.Partition.
 Require Import Crypto.Arithmetic.Saturated.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.ListUtil.
@@ -77,7 +78,7 @@ Module Freeze.
                    | rewrite Rows.conditional_add_partitions
                    | rewrite Rows.sub_partitions
                    | rewrite Rows.sub_div
-                   | rewrite Partition.eval_partition
+                   | rewrite eval_partition
                    | progress distr_length
                    | progress pull_Zmod (*
                    | progress break_innermost_match_step
@@ -115,7 +116,7 @@ Module Freeze.
           (Hp : 0 <= Positional.eval weight n p < 2*modulus)
           (Hplen : length p = n)
           (Hmlen : length m = n)
-      : @freeze n mask m p = Partition.partition weight n (Positional.eval weight n p mod modulus).
+      : @freeze n mask m p = partition weight n (Positional.eval weight n p mod modulus).
     Proof using wprops.
       pose proof (@weight_positive weight wprops n).
       pose proof (fun v => Z.mod_pos_bound v (weight n) ltac:(lia)).
@@ -124,7 +125,7 @@ Module Freeze.
       erewrite <- eval_freeze by eassumption.
       cbv [freeze]; eta_expand.
       rewrite Rows.conditional_add_partitions by (auto; rewrite Rows.sub_partitions; auto; distr_length).
-      rewrite !Partition.eval_partition by assumption.
+      rewrite !eval_partition by assumption.
       apply Partition.partition_Proper; [ assumption .. | ].
       cbv [Z.equiv_modulo].
       pull_Zmod; reflexivity.
@@ -251,7 +252,7 @@ Section freeze_mod_ops.
     : forall (f : list Z)
              (Hf : length f = n)
              (Hf_small : 0 <= eval weight n f < weight n),
-      to_bytes f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f).
+      to_bytes f = partition bytes_weight bytes_n (Positional.eval weight n f).
   Proof using Hn_nz limbwidth_good.
     clear -Hn_nz limbwidth_good.
     intros; cbv [to_bytes].
@@ -264,7 +265,7 @@ Section freeze_mod_ops.
              (Hf : length f = n)
              (Hf_small : 0 <= eval weight n f < weight n),
       eval bytes_weight bytes_n (to_bytesmod f) = eval weight n f
-      /\ to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f).
+      /\ to_bytesmod f = partition bytes_weight bytes_n (Positional.eval weight n f).
   Proof using Hn_nz limbwidth_good.
     split; apply eval_to_bytes || apply to_bytes_partitions; assumption.
   Qed.
@@ -274,7 +275,7 @@ Section freeze_mod_ops.
         (Hf : length f = n)
         (Hf_bounded : 0 <= eval weight n f < 2 * m),
       (eval bytes_weight bytes_n (freeze_to_bytesmod f)) = (eval weight n f) mod m
-      /\ freeze_to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f mod m).
+      /\ freeze_to_bytesmod f = partition bytes_weight bytes_n (Positional.eval weight n f mod m).
   Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded.
     clear -m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded.
     intros; subst m s.
@@ -298,7 +299,7 @@ Section freeze_mod_ops.
     : forall (f : list Z)
         (Hf : length f = n)
         (Hf_bounded : 0 <= eval weight n f < 2 * m),
-      freeze_to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f mod m).
+      freeze_to_bytesmod f = partition bytes_weight bytes_n (Positional.eval weight n f mod m).
   Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded.
     intros; now apply eval_freeze_to_bytesmod_and_partitions.
   Qed.
@@ -319,7 +320,7 @@ Section freeze_mod_ops.
   Lemma from_bytes_partitions
     : forall (f : list Z)
              (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n),
-      from_bytes f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f).
+      from_bytes f = partition weight n (Positional.eval bytes_weight bytes_n f).
   Proof using limbwidth_good.
     clear -limbwidth_good.
     intros; cbv [from_bytes].
@@ -336,7 +337,7 @@ Section freeze_mod_ops.
   Lemma from_bytesmod_partitions
     : forall (f : list Z)
              (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n),
-      from_bytesmod f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f).
+      from_bytesmod f = partition weight n (Positional.eval bytes_weight bytes_n f).
   Proof using limbwidth_good. apply from_bytes_partitions. Qed.
 
   Lemma eval_from_bytesmod_and_partitions
@@ -344,7 +345,7 @@ Section freeze_mod_ops.
              (Hf : length f = bytes_n)
              (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n),
       eval weight n (from_bytesmod f) = eval bytes_weight bytes_n f
-      /\ from_bytesmod f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f).
+      /\ from_bytesmod f = partition weight n (Positional.eval bytes_weight bytes_n f).
   Proof using limbwidth_good Hn_nz.
     now (split; [ apply eval_from_bytesmod | apply from_bytes_partitions ]).
   Qed.
diff --git a/src/Arithmetic/WordByWordMontgomery.v b/src/Arithmetic/WordByWordMontgomery.v
index 2477d212e..3fb3437c1 100644
--- a/src/Arithmetic/WordByWordMontgomery.v
+++ b/src/Arithmetic/WordByWordMontgomery.v
@@ -34,7 +34,7 @@ Module WordByWordMontgomery.
   Section with_args.
     Context (lgr : Z)
             (m : Z).
-    Local Notation weight := (UniformWeight.uweight lgr).
+    Local Notation weight := (uweight lgr).
     Let T (n : nat) := list Z.
     Let r := (2^lgr).
     Definition eval {n} : T n -> Z := Positional.eval weight n.
@@ -138,7 +138,7 @@ Module WordByWordMontgomery.
 
     Local Lemma r_big : r > 1.
     Proof using lgr_big. clear -lgr_big; subst r. auto with zarith. Qed.
-    Local Notation wprops := (@UniformWeight.uwprops lgr lgr_big).
+    Local Notation wprops := (@uwprops lgr lgr_big).
 
     Local Hint Immediate (wprops).
     Local Hint Immediate (weight_0 wprops).
@@ -155,8 +155,8 @@ Module WordByWordMontgomery.
     Lemma R_plusR_le : R + R <= weight (S R_numlimbs).
     Proof using lgr_big.
       clear - lgr_big.
-      etransitivity; [ | apply UniformWeight.uweight_double_le; omega ].
-      rewrite UniformWeight.uweight_eq_alt by omega.
+      etransitivity; [ | apply uweight_double_le; omega ].
+      rewrite uweight_eq_alt by omega.
       subst r R; omega.
     Qed.
 
@@ -165,7 +165,7 @@ Module WordByWordMontgomery.
     Proof using lgr_big.
       clear - lgr_big. cbv [partition].
       rewrite map_map. apply map_ext; intros.
-      rewrite UniformWeight.uweight_S by omega.
+      rewrite uweight_S by omega.
       rewrite <-Z.mod_pull_div by auto with zarith.
       replace (r - 1) with (Z.ones lgr) by (rewrite Z.ones_equiv; subst r; reflexivity).
       rewrite <-Z.land_comm, Z.land_ones by omega.
@@ -226,7 +226,7 @@ Module WordByWordMontgomery.
               | [ H : small ?v |- context[length ?v] ] => erewrite length_small by eassumption
               end
             | rewrite Positional.eval_cons by distr_length
-            | progress rewrite ?weight_0, ?UniformWeight.uweight_1 by auto;
+            | progress rewrite ?weight_0, ?uweight_1 by auto;
               autorewrite with zsimplify_fast
             | rewrite (weight_0 wprops)
             | rewrite <- Z.div_mod'' by auto with omega
@@ -257,7 +257,7 @@ Module WordByWordMontgomery.
              | _ => progress cbn [recursive_partition]
              | H : small _ |- _ => rewrite H; clear H
              | _ => rewrite recursive_partition_equiv by auto using wprops
-             | _ => rewrite UniformWeight.uweight_eval_shift by distr_length
+             | _ => rewrite uweight_eval_shift by distr_length
              | _ => progress push
              end.
 
@@ -280,7 +280,7 @@ Module WordByWordMontgomery.
       clear - r_big lgr_big. intros; autounfold with loc.
       push_recursive_partition. cbn [Rows.divmod fst tl].
       rewrite <-recursive_partition_equiv by auto.
-      rewrite <-UniformWeight.uweight_recursive_partition_equiv with (i:=1%nat) by omega.
+      rewrite <-uweight_recursive_partition_equiv with (i:=1%nat) by omega.
       push.
       apply Partition.partition_Proper; [ solve [auto] | ].
       cbv [Z.equiv_modulo]. autorewrite with zsimplify.
@@ -319,7 +319,7 @@ Module WordByWordMontgomery.
         rewrite weight_0 by auto.
         autorewrite with push_eval zsimplify_fast.
         split; [reflexivity | ].
-        rewrite UniformWeight.uweight_S, UniformWeight.uweight_eq_alt by omega.
+        rewrite uweight_S, uweight_eq_alt by omega.
         subst r; nia. }
     Qed.
 
@@ -331,7 +331,7 @@ Module WordByWordMontgomery.
       clear -lgr_big Ha Hb.
       autounfold with loc; destruct (zerop n); subst.
       { destruct a, b; cbn; try omega; split; auto with zarith. }
-      { pose proof (UniformWeight.uweight_double_le lgr ltac:(omega) n).
+      { pose proof (uweight_double_le lgr ltac:(omega) n).
         eta_expand; split; [ | lia ].
         rewrite Rows.add_partitions, Rows.add_div by auto.
         rewrite partition_step.
@@ -345,7 +345,7 @@ Module WordByWordMontgomery.
       autounfold with loc in *; subst; intros.
       rewrite Rows.add_partitions by auto using Positional.length_extend_to_length.
       autorewrite with push_eval.
-      split; try apply partition_eq_mod; auto; rewrite UniformWeight.uweight_eq_alt by omega; subst r; Z.rewrite_mod_small; auto with zarith.
+      split; try apply partition_eq_mod; auto; rewrite uweight_eq_alt by omega; subst r; Z.rewrite_mod_small; auto with zarith.
     Qed.
 
     Local Lemma conditional_sub_correct : forall v, small v -> 0 <= eval v < eval N + R -> canon_rep (eval v + if eval N <=? eval v then -eval N else 0) (conditional_sub v N).
@@ -356,12 +356,12 @@ Module WordByWordMontgomery.
       repeat match goal with H : small _ |- _ =>
                              rewrite H; clear H end.
       autorewrite with push_eval.
-      assert (weight R_numlimbs < weight (S R_numlimbs)) by (rewrite !UniformWeight.uweight_eq_alt by omega; autorewrite with push_Zof_nat; auto with zarith).
+      assert (weight R_numlimbs < weight (S R_numlimbs)) by (rewrite !uweight_eq_alt by omega; autorewrite with push_Zof_nat; auto with zarith).
       assert (eval N mod weight R_numlimbs < weight (S R_numlimbs)) by (pose proof (Z.mod_pos_bound (eval N) (weight R_numlimbs) ltac:(auto)); omega).
       rewrite Rows.conditional_sub_partitions by (repeat (autorewrite with distr_length push_eval; auto using partition_eq_mod with zarith)).
       rewrite drop_high_to_length_partition by omega.
       autorewrite with push_eval.
-      assert (weight R_numlimbs = R) by (rewrite UniformWeight.uweight_eq_alt by omega; subst R; reflexivity).
+      assert (weight R_numlimbs = R) by (rewrite uweight_eq_alt by omega; subst R; reflexivity).
       Z.rewrite_mod_small.
       break_match; autorewrite with zsimplify_fast; Z.ltb_to_lt.
       { split; [ reflexivity | ].
@@ -379,7 +379,7 @@ Module WordByWordMontgomery.
                              rewrite H; clear H end.
       rewrite Rows.sub_then_maybe_add_partitions by (autorewrite with push_eval distr_length; auto with zarith).
       autorewrite with push_eval.
-      assert (weight R_numlimbs = R) by (rewrite UniformWeight.uweight_eq_alt by omega; subst r R; reflexivity).
+      assert (weight R_numlimbs = R) by (rewrite uweight_eq_alt by omega; subst r R; reflexivity).
       Z.rewrite_mod_small.
       split; [ reflexivity | ].
       break_match; Z.ltb_to_lt; lia.
@@ -972,7 +972,7 @@ Module WordByWordMontgomery.
             (n : nat)
             (m : Z).
     Let r := 2^bitwidth.
-    Local Notation weight := (UniformWeight.uweight bitwidth).
+    Local Notation weight := (uweight bitwidth).
     Local Notation eval := (@eval bitwidth n).
     Let m_enc := partition weight n m.
     Local Coercion Z.of_nat : nat >-> Z.
@@ -985,7 +985,7 @@ Module WordByWordMontgomery.
             (n_nz : n <> 0%nat)
             (m_small : m < r^n).
 
-    Local Notation wprops := (@UniformWeight.uwprops bitwidth bitwidth_big).
+    Local Notation wprops := (@uwprops bitwidth bitwidth_big).
     Local Notation small := (@small bitwidth n).
 
     Local Hint Immediate (wprops).
@@ -998,7 +998,7 @@ Module WordByWordMontgomery.
     Proof using m_small m_big bitwidth_big.
       clear -m_small m_big bitwidth_big.
       cbv [eval m_enc]; autorewrite with push_eval; auto.
-      rewrite UniformWeight.uweight_eq_alt by omega.
+      rewrite uweight_eq_alt by omega.
       Z.rewrite_mod_small; reflexivity.
     Qed.
     Local Lemma r'_pow_correct : (r'^n * r^n) mod (eval m_enc) = 1.
@@ -1012,7 +1012,7 @@ Module WordByWordMontgomery.
     Proof using m_small m_big bitwidth_big.
       clear -m_small m_big bitwidth_big.
       cbv [m_enc small eval]; autorewrite with push_eval; auto.
-      rewrite UniformWeight.uweight_eq_alt by omega.
+      rewrite uweight_eq_alt by omega.
       Z.rewrite_mod_small; reflexivity.
     Qed.
 
@@ -1029,7 +1029,7 @@ Module WordByWordMontgomery.
              | _ => exact small_m_enc
              | [ H : small ?x |- context[eval ?x] ]
                => rewrite H; cbv [eval]; rewrite eval_partition by auto
-             | [ |- context[weight _] ] => rewrite UniformWeight.uweight_eq_alt by auto with omega
+             | [ |- context[weight _] ] => rewrite uweight_eq_alt by auto with omega
              | _=> progress Z.rewrite_mod_small
              | _ => progress Z.zero_bounds
              | [ |- _ mod ?x < ?x ] => apply Z.mod_pos_bound
@@ -1142,7 +1142,7 @@ Module WordByWordMontgomery.
     Local Ltac t_valid v :=
       cbv [valid]; repeat apply conj;
       auto; cbv [small eval]; autorewrite with push_eval; auto;
-      rewrite ?UniformWeight.uweight_eq_alt by omega;
+      rewrite ?uweight_eq_alt by omega;
       Z.rewrite_mod_small;
       rewrite ?(Z.mod_small (_ mod m)) by (subst r; Z.div_mod_to_quot_rem; lia);
       rewrite ?(Z.mod_small v) by (subst r; Z.div_mod_to_quot_rem; lia);
@@ -1155,7 +1155,7 @@ Module WordByWordMontgomery.
         [ | now t_valid v.. ].
       push_Zmod; rewrite !eval_from_montgomerymod; [ | now t_valid v.. ].
       cbv [eval]; autorewrite with push_eval; auto.
-      rewrite ?UniformWeight.uweight_eq_alt by omega.
+      rewrite ?uweight_eq_alt by omega.
       rewrite ?(Z.mod_small v) by (subst r; Z.div_mod_to_quot_rem; lia).
       rewrite ?(Z.mod_small (_ mod m)) by (subst r; Z.div_mod_to_quot_rem; lia).
       pull_Zmod.
@@ -1258,16 +1258,16 @@ Module WordByWordMontgomery.
     Qed.
 
     Lemma to_bytesmod_correct
-      : (forall a (_ : valid a), Positional.eval (UniformWeight.uweight 8) (bytes_n bitwidth 1 n) (to_bytesmod a)
+      : (forall a (_ : valid a), Positional.eval (uweight 8) (bytes_n bitwidth 1 n) (to_bytesmod a)
                                  = eval a mod m)
-        /\ (forall a (_ : valid a), to_bytesmod a = partition (UniformWeight.uweight 8) (bytes_n bitwidth 1 n) (eval a mod m)).
+        /\ (forall a (_ : valid a), to_bytesmod a = partition (uweight 8) (bytes_n bitwidth 1 n) (eval a mod m)).
     Proof using n_nz m_small bitwidth_big.
       clear -n_nz m_small bitwidth_big.
       generalize (@length_small bitwidth n);
         cbv [valid small to_bytesmod eval]; split; intros; (etransitivity; [ apply eval_to_bytesmod | ]);
-          fold weight in *; fold (UniformWeight.uweight 8) in *; subst r;
+          fold weight in *; fold (uweight 8) in *; subst r;
           try solve [ intuition eauto with omega ].
-      all: repeat first [ rewrite UniformWeight.uweight_eq_alt by omega
+      all: repeat first [ rewrite uweight_eq_alt by omega
                         | omega
                         | reflexivity
                         | progress Z.rewrite_mod_small ].
@@ -1275,7 +1275,7 @@ Module WordByWordMontgomery.
 
     Lemma eval_to_bytesmod
       : (forall a (_ : valid a),
-            Positional.eval (UniformWeight.uweight 8) (bytes_n bitwidth 1 n) (to_bytesmod a)
+            Positional.eval (uweight 8) (bytes_n bitwidth 1 n) (to_bytesmod a)
             = eval a mod m).
     Proof. apply to_bytesmod_correct. Qed.
   End modops.
diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v
index 19014ffec..3946a39c2 100644
--- a/src/PushButtonSynthesis/BarrettReduction.v
+++ b/src/PushButtonSynthesis/BarrettReduction.v
@@ -30,7 +30,7 @@ Import Compilers.defaults.
 Import COperationSpecifications.Primitives.
 Import COperationSpecifications.BarrettReduction.
 
-Import Associational Positional Arithmetic.BarrettReduction.
+Import Associational Positional.
 
 Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *)
 
@@ -71,12 +71,12 @@ Section rbarrett_red.
 
   Lemma mut_correct :
     0 < machine_wordsize ->
-    Partition.partition (UniformWeight.uweight machine_wordsize) (1 + 1) (muLow + 2 ^ machine_wordsize) = [muLow; 1].
+    partition (uweight machine_wordsize) (1 + 1) (muLow + 2 ^ machine_wordsize) = [muLow; 1].
   Proof.
     intros; cbn. subst muLow.
     assert (0 < 2^machine_wordsize) by ZeroBounds.Z.zero_bounds.
     pose proof (Z.mod_pos_bound mu (2^machine_wordsize) ltac:(lia)).
-    rewrite !UniformWeight.uweight_S, weight_0; auto using UniformWeight.uwprops with lia.
+    rewrite !uweight_S, weight_0; auto using uwprops with lia.
     autorewrite with zsimplify.
     Modulo.push_Zmod. autorewrite with zsimplify. Modulo.pull_Zmod.
     rewrite <-Modulo.Z.mod_pull_div by lia.
@@ -86,10 +86,10 @@ Section rbarrett_red.
   Lemma Mt_correct :
     0 < machine_wordsize ->
     2^(machine_wordsize - 1) < M < 2^machine_wordsize ->
-    Partition.partition (UniformWeight.uweight machine_wordsize) 1 M = [M].
+    partition (uweight machine_wordsize) 1 M = [M].
   Proof.
     intros; cbn. assert (0 < 2^(machine_wordsize-1)) by ZeroBounds.Z.zero_bounds.
-    rewrite !UniformWeight.uweight_S, weight_0; auto using UniformWeight.uwprops with lia.
+    rewrite !uweight_S, weight_0; auto using uwprops with lia.
     autorewrite with zsimplify. RewriteModSmall.Z.rewrite_mod_small.
     reflexivity.
   Qed.
@@ -177,7 +177,7 @@ Section rbarrett_red.
                  | progress cbv [weight]
                  | rewrite mut_correct
                  | rewrite Mt_correct
-                 | rewrite UniformWeight.uweight_eq_alt'
+                 | rewrite uweight_eq_alt'
                  | rewrite Z.pow_mul_r by lia ].
 
   Local Strategy -100 [barrett_red]. (* needed for making Qed not take forever *)
diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v
index aae25a578..5743d2c6a 100644
--- a/src/PushButtonSynthesis/WordByWordMontgomery.v
+++ b/src/PushButtonSynthesis/WordByWordMontgomery.v
@@ -99,7 +99,7 @@ Section __.
             end.
   Let n_bytes := bytes_n machine_wordsize 1 n.
   Let prime_upperbound_list : list Z
-    := Partition.partition (UniformWeight.uweight machine_wordsize) n (s-1).
+    := Partition.partition (uweight machine_wordsize) n (s-1).
   Let prime_bytes_upperbound_list : list Z
     := Partition.partition (weight 8 1) n_bytes (s-1).
   Let upperbounds : list Z := prime_upperbound_list.
@@ -140,8 +140,8 @@ Section __.
             (negb ((r * r') mod m =? 1)%Z, Pipeline.Values_not_provably_equalZ "(r * r') mod m ≠ 1" ((r * r') mod m) 1);
             (negb ((m * m') mod r =? (-1) mod r)%Z, Pipeline.Values_not_provably_equalZ "(m * m') mod r ≠ (-1) mod r" ((m * m') mod r) ((-1) mod r));
             (negb (s <=? r^n), Pipeline.Value_not_leZ "r^n ≤ s" s (r^n));
-            (negb (s <=? UniformWeight.uweight machine_wordsize n), Pipeline.Value_not_leZ "weight n < s (needed for from_bytes)" s (UniformWeight.uweight machine_wordsize n));
-            (negb (UniformWeight.uweight machine_wordsize n =? UniformWeight.uweight 8 n_bytes), Pipeline.Values_not_provably_equalZ "weight n ≠ bytes_weight n_bytes (needed for from_bytes)" (UniformWeight.uweight machine_wordsize n) (UniformWeight.uweight 8 n_bytes))].
+            (negb (s <=? uweight machine_wordsize n), Pipeline.Value_not_leZ "weight n < s (needed for from_bytes)" s (uweight machine_wordsize n));
+            (negb (uweight machine_wordsize n =? uweight 8 n_bytes), Pipeline.Values_not_provably_equalZ "weight n ≠ bytes_weight n_bytes (needed for from_bytes)" (uweight machine_wordsize n) (uweight 8 n_bytes))].
 
   Local Arguments Z.mul !_ !_.
   Local Ltac use_curve_good_t :=
@@ -179,9 +179,9 @@ Section __.
       /\ 1 < m
       /\ m < r^n
       /\ s = 2^Z.log2 s
-      /\ s <= UniformWeight.uweight machine_wordsize n
-      /\ s <= UniformWeight.uweight 8 n_bytes
-      /\ UniformWeight.uweight machine_wordsize n = UniformWeight.uweight 8 n_bytes.
+      /\ s <= uweight machine_wordsize n
+      /\ s <= uweight 8 n_bytes
+      /\ uweight machine_wordsize n = uweight 8 n_bytes.
   Proof.
     clear -curve_good.
     cbv [check_args fold_right] in curve_good.
@@ -520,10 +520,10 @@ Section __.
     { cbv [Partition.partition seq map In]; tauto. }
     { intros *; rewrite Partition.partition_step, in_app_iff; cbn [List.In].
       intros; destruct_head'_or; subst *; eauto; try tauto; [].
-      rewrite UniformWeight.uweight_S by lia.
-      assert (0 < UniformWeight.uweight machine_wordsize n') by now apply UniformWeight.uwprops.
+      rewrite uweight_S by lia.
+      assert (0 < uweight machine_wordsize n') by now apply uwprops.
       assert (0 < 2 ^ machine_wordsize) by auto with zarith.
-      assert (0 < 2 ^ machine_wordsize * UniformWeight.uweight machine_wordsize n') by nia.
+      assert (0 < 2 ^ machine_wordsize * uweight machine_wordsize n') by nia.
       rewrite <- Z.mod_pull_div by lia.
       rewrite Z.le_sub_1_iff.
       auto with zarith. }
@@ -533,9 +533,9 @@ Section __.
   Lemma bounded_by_prime_bounds_of_valid_gen lgr n' x
         (Hlgr : 0 < lgr)
         (Hs : s = 2^Z.log2 s)
-        (Hs' : s <= UniformWeight.uweight lgr n')
+        (Hs' : s <= uweight lgr n')
         (H : WordByWordMontgomery.valid lgr n' m x)
-    : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some (List.map (fun v => Some r[0~>v]%zrange) (Partition.partition (UniformWeight.uweight lgr) n' (s-1)))) x = true.
+    : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some (List.map (fun v => Some r[0~>v]%zrange) (Partition.partition (uweight lgr) n' (s-1)))) x = true.
   Proof using curve_good.
     pose proof use_curve_good as use_curve_good.
     clear -H use_curve_good curve_good Hlgr Hs Hs'.
@@ -567,13 +567,13 @@ Section __.
     assert (1 < 2^Z.log2 s) by auto with zarith.
     generalize dependent (Z.log2 s); intro lgs; intros.
 
-    edestruct (UniformWeight.uwprops lgr); try lia.
-    assert (forall i : nat, 0 <= UniformWeight.uweight lgr i) by (intro z; specialize (weight_positive z); lia).
+    edestruct (uwprops lgr); try lia.
+    assert (forall i : nat, 0 <= uweight lgr i) by (intro z; specialize (weight_positive z); lia).
     apply Bool.andb_true_intro; split; apply OrdersEx.Z_as_OT.leb_le;
       [apply Z.div_nonneg | apply Z.div_le_mono_nonneg]; trivial.
     apply Z.mod_pos_bound; trivial.
 
-    cbv [UniformWeight.uweight].
+    cbv [uweight].
     cbv [weight].
     rewrite Z.div_1_r.
     rewrite Z.opp_involutive.
@@ -632,12 +632,12 @@ Section __.
     cbv [bytes_valid] in H.
     destruct H as [_ H].
     pose proof use_curve_good.
-    cbv [UniformWeight.uweight] in *; destruct_head'_and; lia.
+    cbv [uweight] in *; destruct_head'_and; lia.
   Qed.
 
   Local Ltac solve_extra_bounds_side_conditions :=
     solve [ cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia
-          | cbv [valid small eval UniformWeight.uweight n_bytes] in *; destruct_head'_and; auto
+          | cbv [valid small eval uweight n_bytes] in *; destruct_head'_and; auto
           | now apply weight_bounded_of_bytes_valid
           | eapply length_of_valid; eassumption ].
 
@@ -702,7 +702,7 @@ Section __.
                  | progress autorewrite with interp interp_gen_cache push_eval
                  | progress autounfold with push_eval
                  | progress autorewrite with distr_length in *
-                 | solve [ cbv [valid small eval UniformWeight.uweight n_bytes] in *; destruct_head'_and; auto ] ].
+                 | solve [ cbv [valid small eval uweight n_bytes] in *; destruct_head'_and; auto ] ].
 
   (** TODO: DESIGN DECISION: