Don't inline everything in Montgomery and Barrett

We still use CSE in fancy machine, because we want to lift the ldi's
above the rest of the code.  However, on a quick inspection, the
algorithm no longer needs CSE to be duplicate-free.

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;