diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-13 13:58:46 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-13 13:58:46 -0400 |
| commit | 2854cff14f95693819d42b611fe75a4904d9c77d (patch) | |
| tree | c105298f538c87a2bd0ac19d1a4e273827e0709d /src/Specific/FancyMachine256/Barrett.v | |
| parent | de7a98b8711f13f9b9bba016c1d19db730479c8e (diff) | |
Support destructuring dlet and slet
The current way to support it is a kludge around the fact that `x
binder` only works for recursive notations
Diffstat (limited to 'src/Specific/FancyMachine256/Barrett.v')
| -rw-r--r-- | src/Specific/FancyMachine256/Barrett.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Specific/FancyMachine256/Barrett.v b/src/Specific/FancyMachine256/Barrett.v index 263bc82ba..6bd97b10c 100644 --- a/src/Specific/FancyMachine256/Barrett.v +++ b/src/Specific/FancyMachine256/Barrett.v @@ -129,9 +129,9 @@ Print compiled_syntax. (* compiled_syntax = fun ops : fancy_machine.instructions (2 * 128) => λn (RegMod, RegMuLow, x, xHigh), -slet RegMod := RegMod in -slet RegMuLow := RegMuLow in -slet RegZero := ldi 0 in +nlet RegMod := RegMod in +nlet RegMuLow := RegMuLow in +nlet RegZero := ldi 0 in c.Rshi(tmp, xHigh, x, 250), c.Mul128(q, c.LowerHalf(tmp), c.LowerHalf(RegMuLow)), c.Mul128(qHigh, c.UpperHalf(tmp), c.UpperHalf(RegMuLow)), |