diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-03 18:10:18 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-03 18:10:18 -0400 |
commit | 4f5c10812f02c056fed7478c2da1543aec84d8fe (patch) | |
tree | 3bd2ac15447347e62a5aab9562c9ff4ace957bff /src/ModularArithmetic/ModularBaseSystemProofs.v | |
parent | 9b318933ba8ba83f063008831c4c79da4897e5e1 (diff) |
Fix 8.4 build partially
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. |