diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-05-14 19:53:49 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-05-14 19:53:49 -0400 |
| commit | 9b70845270bcb21f461e908030a1b8559ef4429a (patch) | |
| tree | 998d5f2e4269ec7bf7a09cbdbfefdaeb2d8eab78 /src/Arithmetic/Core.v | |
| parent | df26ed5072ba2c44234493afe050b0e162f59f35 (diff) | |
force carry intermediates to be bound early
Diffstat (limited to 'src/Arithmetic/Core.v')
| -rw-r--r-- | src/Arithmetic/Core.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index f294c06fc..b86ac09b9 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -430,7 +430,9 @@ Module B. Definition carryterm_cps (w fw:Z) (t:limb) {T} (f:list limb->T) := if dec (fst t = w) then dlet t2 := snd t in - f ((w*fw, div t2 fw) :: (w, modulo t2 fw) :: @nil limb) + dlet d2 := div t2 fw in + dlet m2 := modulo t2 fw in + f ((w*fw, d2) :: (w, m2) :: @nil limb) else f [t]. Definition carryterm w fw t := carryterm_cps w fw t id. |