diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-19 16:55:50 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-19 16:56:00 -0400 |
| commit | fd61b21d4244866f3a3190e110cba0a80382d6ff (patch) | |
| tree | 6ede1ec429ebf39449ec6e4a445d80e1ad23674a /src/Arithmetic | |
| parent | 21f4efcf4156440fed5428e045112565aa054d21 (diff) | |
Use fold_right_cps2 to get eqb_cps to get the right continuation type
Diffstat (limited to 'src/Arithmetic')
| -rw-r--r-- | src/Arithmetic/Core.v | 6 | ||||
| -rw-r--r-- | src/Arithmetic/Saturated/Core.v | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index f2d9ee00b..5104a21aa 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -614,10 +614,10 @@ Module B. Definition from_associational_cps n (p:list limb) {T} (f:tuple Z n->T):= - fold_right_cps - (fun t st => + fold_right_cps2 + (fun t st T' f' => place_cps t (pred n) - (fun p=> add_to_nth_cps (fst p) (snd p) st id)) + (fun p=> add_to_nth_cps (fst p) (snd p) st f')) (zeros n) p f. Definition from_associational n p := from_associational_cps n p id. 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. |