From a6fe61b6001857907f40f54e45964d46b754a30d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Jun 2017 13:43:03 -0400 Subject: Fix the sense of op_{get,with}_carry in Saturated Now it lines up with the things in Z.Definitions --- src/Arithmetic/Saturated.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index 5ecb5eebd..14f689322 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -735,10 +735,10 @@ Module Positional. | None => op_get_carry | Some x => op_with_carry x end in dlet carry_result := op' (hd p) (hd q) in - chain_op'_cps (Some (fst carry_result)) (tl p) (tl q) _ + chain_op'_cps (Some (snd carry_result)) (tl p) (tl q) _ (fun carry_pq => f (fst carry_pq, - append (snd carry_result) (snd carry_pq))) + append (fst carry_result) (snd carry_pq))) end. Definition chain_op' {n} c p q := @chain_op'_cps n c p q _ id. Definition chain_op_cps {n} p q {T} f := @chain_op'_cps n None p q T f. -- cgit v1.2.3