diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-09-22 14:25:26 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-09-22 14:58:53 -0400 |
| commit | f7e7c340ab08de79db745db5d2b699dd99dc407a (patch) | |
| tree | a51dfdf846280e6ef441d0859662d5b40d3e8a99 /src/Specific/FancyMachine256 | |
| parent | 8ee7882b46d4b8aba92fed51391d03ae8d418a43 (diff) | |
Use dlet, not llet
Diffstat (limited to 'src/Specific/FancyMachine256')
| -rw-r--r-- | src/Specific/FancyMachine256/Barrett.v | 5 | ||||
| -rw-r--r-- | src/Specific/FancyMachine256/Core.v | 2 | ||||
| -rw-r--r-- | src/Specific/FancyMachine256/Montgomery.v | 5 |
3 files changed, 7 insertions, 5 deletions
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 |