diff options
Diffstat (limited to 'src/BoundedArithmetic/ArchitectureToZLike.v')
-rw-r--r-- | src/BoundedArithmetic/ArchitectureToZLike.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/BoundedArithmetic/ArchitectureToZLike.v b/src/BoundedArithmetic/ArchitectureToZLike.v index 3388ece78..80f0d9803 100644 --- a/src/BoundedArithmetic/ArchitectureToZLike.v +++ b/src/BoundedArithmetic/ArchitectureToZLike.v @@ -4,6 +4,7 @@ Require Import Crypto.BoundedArithmetic.Interface. Require Import Crypto.BoundedArithmetic.DoubleBounded. Require Import Crypto.ModularArithmetic.ZBounded. Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.LockedLet. Local Open Scope Z_scope. @@ -23,7 +24,7 @@ Section fancy_machine_p256_montgomery_foundation. DivBy_SmallBound v := snd v; DivBy_SmallerBound v := if smaller_bound_exp =? n then snd v - else shrd (snd v) (fst v) smaller_bound_exp; + else llet v := v in shrd (snd v) (fst v) smaller_bound_exp; Mul x y := muldw x y; CarryAdd x y := adc x y false; CarrySubSmall x y := subc x y false; |