Use dlet, not llet

1 files changed, 2 insertions, 2 deletions

diff --git a/src/BoundedArithmetic/ArchitectureToZLike.v b/src/BoundedArithmetic/ArchitectureToZLike.v
index 80f0d9803..e37932192 100644
--- a/src/BoundedArithmetic/ArchitectureToZLike.v
+++ b/src/BoundedArithmetic/ArchitectureToZLike.v
@@ -4,7 +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.
+Require Import Crypto.Util.LetIn.
 
 Local Open Scope Z_scope.
 
@@ -24,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 llet v := v in shrd (snd v) (fst v) smaller_bound_exp;
+                              else dlet 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;