diff options
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 197a0dca6..3b0231191 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -532,7 +532,7 @@ Class FreezePreconditions `{prm : PseudoMersenneBaseParams} B int_width := c_reduce1 : c * ((2 ^ B) >> nth_default 0 limb_widths (pred (length limb_widths))) <= 2 ^ (nth_default 0 limb_widths 0); (* on the second reduce step, we add at most one bit of width to the first digit, and leave room to carry c one more time after the highest bit is carried *) - c_reduce2 : c <= 2 ^ (nth_default 0 limb_widths 0) - c; + c_reduce2 : c <= 2 ^ (nth_default 0 limb_widths 0) - c }. Section CanonicalizationProofs. |