aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/Saturated/Core.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Arithmetic/Saturated/Core.v')
-rw-r--r--src/Arithmetic/Saturated/Core.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Arithmetic/Saturated/Core.v b/src/Arithmetic/Saturated/Core.v
index 8af1cce6f..2118fcdfc 100644
--- a/src/Arithmetic/Saturated/Core.v
+++ b/src/Arithmetic/Saturated/Core.v
@@ -394,10 +394,10 @@ Module Columns.
Definition from_associational_cps n (p:list B.limb)
{T} (f:(list Z)^n -> T) :=
- fold_right_cps
- (fun t st =>
+ fold_right_cps2
+ (fun t st T' f' =>
B.Positional.place_cps weight t (pred n)
- (fun p=> cons_to_nth_cps (fst p) (snd p) st id))
+ (fun p=> cons_to_nth_cps (fst p) (snd p) st f'))
(nils n) p f.
Definition from_associational n p := from_associational_cps n p id.