diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-07 01:03:33 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-07 01:03:41 -0500 |
| commit | 538a0b6a0c61458133d146d79834fde4d2364546 (patch) | |
| tree | 85012ec96076f4f4a109e70851c5c53d06844e66 /src/Arithmetic | |
| parent | e82f495c3fcdd037e85708b23c11abc37de5d918 (diff) | |
More use of Z.eqb_cps
Diffstat (limited to 'src/Arithmetic')
| -rw-r--r-- | src/Arithmetic/Core.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index a33bd394d..cfcc71e65 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -448,14 +448,15 @@ Module B. Hint Rewrite modulo_cps_id div_cps_id : uncps. Definition carryterm_cps (w fw:Z) (t:limb) {T} (f:list limb->T) := - if dec (fst t = w) + Z.eqb_cps (fst t) w (fun eqb => + if eqb then dlet t2 := snd t in div_cps _ t2 fw (fun d2 => modulo_cps _ t2 fw (fun m2 => dlet d2 := d2 in dlet m2 := m2 in f ((w*fw, d2) :: (w, m2) :: @nil limb))) - else f [t]. + else f [t]). Definition carryterm w fw t := carryterm_cps w fw t id. Lemma carryterm_cps_id w fw t {T} f : |