Changed name of [carry_and_reduce_single] to [carry_single], since it does not perform reduction

3 files changed, 7 insertions, 7 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index ed8f80659..33b2d7f2d 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -124,7 +124,7 @@ Section Carries.
     rewrite <-from_list_default_eq with (d := 0%Z).
     rewrite <-pull_app_if_sumbool.
     cbv beta delta
-      [carry carry_and_reduce Pow2Base.carry_gen Pow2Base.carry_and_reduce_single Pow2Base.carry_simple
+      [carry carry_and_reduce Pow2Base.carry_gen Pow2Base.carry_single Pow2Base.carry_simple
        Z.pow2_mod Z.ones Z.pred
        PseudoMersenneBaseParams.limb_widths].
     rewrite !add_to_nth_set_nth.
diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v
index c23cf8f40..a2c76016d 100644
--- a/src/ModularArithmetic/Pow2Base.v
+++ b/src/ModularArithmetic/Pow2Base.v
@@ -49,14 +49,14 @@ Section Pow2Base.
 
     Definition add_to_nth n (x:Z) xs :=
       update_nth n (fun y => x + y) xs.
-    Definition carry_and_reduce_single i := fun di =>
+    Definition carry_single i := fun di =>
       (Z.pow2_mod di (log_cap i),
        Z.shiftr di (log_cap i)).
 
     Definition carry_gen fc fi i := fun us =>
       let i := fi (length us) i in
       let di := nth_default 0 us      i in
-      let '(di', ci) := carry_and_reduce_single i di in
+      let '(di', ci) := carry_single i di in
       let us' := set_nth i di' us in
       add_to_nth (fi (length us) (S i)) (fc ci) us'.
 
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v
index 78c6bba0f..9255f033f 100644
--- a/src/ModularArithmetic/Pow2BaseProofs.v
+++ b/src/ModularArithmetic/Pow2BaseProofs.v
@@ -688,7 +688,7 @@ Section carrying.
   Local Hint Resolve limb_widths_nonneg sum_firstn_limb_widths_nonneg.
 
   Lemma length_carry_gen : forall fc fi i us, length (carry_gen limb_widths fc fi i us) = length us.
-  Proof. intros; unfold carry_gen, carry_and_reduce_single; distr_length; reflexivity. Qed.
+  Proof. intros; unfold carry_gen, carry_single; distr_length; reflexivity. Qed.
 
   Hint Rewrite @length_carry_gen : distr_length.
 
@@ -722,14 +722,14 @@ Section carrying.
     destruct (eq_nat_dec 0 (length base));
       [ destruct limb_widths, us, i; simpl in *; try congruence;
         break_match;
-        unfold carry_gen, carry_and_reduce_single, add_to_nth;
+        unfold carry_gen, carry_single, add_to_nth;
         autorewrite with zsimplify simpl_nth_default simpl_set_nth simpl_update_nth distr_length;
         reflexivity
       | ].
     (*assert (0 <= i < length base)%nat by (subst i; auto with arith).*)
     assert (0 <= log_cap i) by auto using log_cap_nonneg.
     assert (2 ^ log_cap i <> 0) by (apply Z.pow_nonzero; lia).
-    unfold carry_gen, carry_and_reduce_single.
+    unfold carry_gen, carry_single.
     rewrite H; change (i' mod length base)%nat with i.
     rewrite add_to_nth_sum by (rewrite length_set_nth; omega).
     rewrite set_nth_sum by omega.
@@ -798,7 +798,7 @@ Section carrying.
              else 0
         else d.
   Proof.
-    unfold carry_gen, carry_and_reduce_single.
+    unfold carry_gen, carry_single.
     intros; autorewrite with push_nth_default natsimplify distr_length.
     edestruct (lt_dec n (length us)) as [H|H]; [ | reflexivity ].
     rewrite !(@nth_default_in_bounds Z 0 d) by assumption.