Use dlet, not llet

7 files changed, 29 insertions, 27 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;
diff --git a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v b/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
index 243ecb064..a7d5242b6 100644
--- a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
+++ b/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
@@ -8,7 +8,7 @@ Require Import Crypto.BoundedArithmetic.ArchitectureToZLike.
 Require Import Crypto.ModularArithmetic.ZBounded.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.
-Require Import Crypto.Util.LockedLet.
+Require Import Crypto.Util.LetIn.
 
 Local Open Scope nat_scope.
 Local Open Scope Z_scope.
@@ -54,7 +54,7 @@ Section fancy_machine_p256_montgomery_foundation.
   Local Ltac post_t_step :=
     match goal with
     | _ => reflexivity
-    | _ => rewrite !unlock_let
+    | _ => progress unfold Let_In
     | _ => progress autorewrite with zsimplify_const
     | [ |- fst ?x = (?a <=? ?b) :> bool ]
       => cut (((if fst x then 1 else 0) = (if a <=? b then 1 else 0))%Z);
diff --git a/src/BoundedArithmetic/DoubleBounded.v b/src/BoundedArithmetic/DoubleBounded.v
index b6aa858ff..5cf48cd3b 100644
--- a/src/BoundedArithmetic/DoubleBounded.v
+++ b/src/BoundedArithmetic/DoubleBounded.v
@@ -6,7 +6,7 @@ Require Import Crypto.ModularArithmetic.Pow2Base.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.LockedLet.
+Require Import Crypto.Util.LetIn.
 
 Local Open Scope nat_scope.
 Local Open Scope Z_scope.
@@ -28,13 +28,13 @@ Section ripple_carry_definitions.
     : forall (xs ys : tuple' T k) (carry : bool), bool * tuple' T k
     := match k return forall (xs ys : tuple' T k) (carry : bool), bool * tuple' T k with
        | O => f
-       | S k' => fun xss yss carry => llet xss := xss in
-                                      llet yss := yss in
+       | S k' => fun xss yss carry => dlet xss := xss in
+                                      dlet yss := yss in
                                       let '(xs, x) := eta xss in
                                       let '(ys, y) := eta yss in
-                                      llet addv := (@ripple_carry_tuple' _ f k' xs ys carry) in
+                                      dlet addv := (@ripple_carry_tuple' _ f k' xs ys carry) in
                                       let '(carry, zs) := eta addv in
-                                      llet fxy := (f x y carry) in
+                                      dlet fxy := (f x y carry) in
                                       let '(carry, z) := eta fxy in
                                       (carry, (zs, z))
        end.
@@ -80,15 +80,15 @@ Section tuple2.
             {ldi : load_immediate W}.
 
     Definition mul_double (a b : W) : tuple W 2
-      := llet a              := a in
-         llet b              := b in
+      := dlet a              := a in
+         dlet b              := b in
          let out : tuple W 2 := (mulhwll a b, mulhwhh a b) in
-         llet out            := out in
-         llet tmp            := mulhwhl a b in
-         llet addv           := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in
+         dlet out            := out in
+         dlet tmp            := mulhwhl a b in
+         dlet addv           := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in
          let '(_, out)       := eta addv in
-         llet tmp            := mulhwhl b a in
-         llet addv           := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in
+         dlet tmp            := mulhwhl b a in
+         dlet addv           := (ripple_carry_adc adc out (shl tmp half_n, shr tmp half_n) false) in
          let '(_, out)       := eta addv in
          out.
 
diff --git a/src/BoundedArithmetic/DoubleBoundedProofs.v b/src/BoundedArithmetic/DoubleBoundedProofs.v
index 95ba35579..d0f782f9a 100644
--- a/src/BoundedArithmetic/DoubleBoundedProofs.v
+++ b/src/BoundedArithmetic/DoubleBoundedProofs.v
@@ -12,7 +12,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.LockedLet.
+Require Import Crypto.Util.LetIn.
 
 Import ListNotations.
 Local Open Scope list_scope.
@@ -239,20 +239,20 @@ Global Instance decode_mul_double
 
 Lemma ripple_carry_tuple_SS' {T} f k xss yss carry
   : @ripple_carry_tuple T f (S (S k)) xss yss carry
-    = llet xss := xss in
-      llet yss := yss in
+    = dlet xss := xss in
+      dlet yss := yss in
       let '(xs, x) := eta xss in
       let '(ys, y) := eta yss in
-      llet addv := (@ripple_carry_tuple _ f (S k) xs ys carry) in
+      dlet addv := (@ripple_carry_tuple _ f (S k) xs ys carry) in
       let '(carry, zs) := eta addv in
-      llet fxy := (f x y carry) in
+      dlet fxy := (f x y carry) in
       let '(carry, z) := eta fxy in
       (carry, (zs, z)).
 Proof. reflexivity. Qed.
 
 Local Ltac eta_expand :=
   repeat match goal with
-         | _ => rewrite !unlock_let
+         | _ => progress unfold Let_In
          | [ |- context[let '(x, y) := ?e in _] ]
            => rewrite (surjective_pairing e)
          | _ => rewrite <- !surjective_pairing
diff --git a/src/Specific/FancyMachine256/Barrett.v b/src/Specific/FancyMachine256/Barrett.v
index fd57f1fa3..4ee4d5579 100644
--- a/src/Specific/FancyMachine256/Barrett.v
+++ b/src/Specific/FancyMachine256/Barrett.v
@@ -44,13 +44,14 @@ Section expression.
   Local Arguments μ' / .
   Local Arguments ldi' / .
   Local Arguments DoubleBounded.mul_double / .
+  Local Opaque Let_In.
 
   Definition expression'
     := Eval simpl in
         (fun v => proj1_sig (pre_f v)).
-  Local Transparent locked_let.
+  Local Transparent Let_In.
   Definition expression
-    := Eval cbv beta iota delta [expression' fst snd locked_let] in
+    := Eval cbv beta iota delta [expression' fst snd Let_In] in
         fun v => let RegMod := fancy_machine.ldi m in
                  let RegMu := fancy_machine.ldi μ in
                  let RegZero := fancy_machine.ldi 0 in
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v
index 419f1a24c..2dc6469bd 100644
--- a/src/Specific/FancyMachine256/Core.v
+++ b/src/Specific/FancyMachine256/Core.v
@@ -20,7 +20,7 @@ Require Export Crypto.Reflection.Reify.
 Require Export Crypto.Util.ZUtil.
 Require Export Crypto.Util.Notations.
 Require Import Crypto.Util.ListUtil.
-Require Export Crypto.Util.LockedLet.
+Require Export Crypto.Util.LetIn.
 Export ListNotations.
 
 Open Scope Z_scope.
diff --git a/src/Specific/FancyMachine256/Montgomery.v b/src/Specific/FancyMachine256/Montgomery.v
index 56879eb57..e25907ebf 100644
--- a/src/Specific/FancyMachine256/Montgomery.v
+++ b/src/Specific/FancyMachine256/Montgomery.v
@@ -28,12 +28,13 @@ Section expression.
   Local Arguments ldi' / .
   Local Arguments reduce_via_partial / .
   Local Arguments DoubleBounded.mul_double / .
+  Local Opaque Let_In.
 
   Definition expression'
     := Eval simpl in f.
-  Local Transparent locked_let.
+  Local Transparent Let_In.
   Definition expression
-    := Eval cbv beta delta [expression' fst snd locked_let] in
+    := Eval cbv beta delta [expression' fst snd Let_In] in
         fun v => let RegMod := fancy_machine.ldi modulus in
                  let RegPInv := fancy_machine.ldi m' in
                  let RegZero := fancy_machine.ldi 0 in