From 4f5c10812f02c056fed7478c2da1543aec84d8fe Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 3 Nov 2016 18:10:18 -0400 Subject: Fix 8.4 build partially --- src/ModularArithmetic/ModularBaseSystemProofs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/ModularArithmetic') 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. -- cgit v1.2.3