diff options
Diffstat (limited to 'src/Arithmetic')
| -rw-r--r-- | src/Arithmetic/Saturated/Core.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Arithmetic/Saturated/Core.v b/src/Arithmetic/Saturated/Core.v index 2118fcdfc..fa7bbe919 100644 --- a/src/Arithmetic/Saturated/Core.v +++ b/src/Arithmetic/Saturated/Core.v @@ -166,7 +166,9 @@ Module Columns. Fixpoint compact_digit_cps (digit : list Z) (f:Z * Z->T) := match digit with | nil => f (0, 0) - | x :: nil => f (div x (weight (S n) / weight n), modulo x (weight (S n) / weight n)) + | x :: nil => div_cps x (weight (S n) / weight n) (fun d => + modulo_cps x (weight (S n) / weight n) (fun m => + f (d, m))) | x :: y :: nil => add_get_carry_cps _ (weight (S n) / weight n) x y (fun sum_carry => dlet sum_carry := sum_carry in |