From 538a0b6a0c61458133d146d79834fde4d2364546 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 7 Nov 2017 01:03:33 -0500
Subject: More use of Z.eqb_cps

---
 src/Arithmetic/Core.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/Arithmetic/Core.v')

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 :
-- 
cgit v1.2.3