diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-01 01:02:25 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-01 01:02:25 -0400 |
| commit | a6e23a285105ff9df74a9728dbf441eb96911dc8 (patch) | |
| tree | 553e47376f1ffa8194a16c7eff5d63463e013fbf /src/Arithmetic | |
| parent | 824e4fff531916aeb0870dfd8d8d51b5c68ebfa4 (diff) | |
More use of Z.eqb_cps
Diffstat (limited to 'src/Arithmetic')
| -rw-r--r-- | src/Arithmetic/Core.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 4df36a0aa..7335f6523 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -249,6 +249,7 @@ Require Import Crypto.Util.Decidable Crypto.Util.LetIn. Require Import Crypto.Util.ZUtil Crypto.Util.ListUtil Crypto.Util.Sigma. Require Import Crypto.Util.CPSUtil Crypto.Util.Prod. Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.CPS. Require Import Crypto.Arithmetic.PrimeFieldTheorems. @@ -279,6 +280,7 @@ Local Ltac prove_eval := | _ => progress intros | _ => progress simpl | _ => progress cbv [Let_In] + | _ => progress Z.ltb_to_lt | _ => progress (autorewrite with push_basesystem_eval uncps push_id cancel_pair in * ) | _ => break_innermost_match_step | _ => split @@ -359,9 +361,11 @@ Module B. | cons x xs' => split_cps xs' (fun sxs' => - if dec (fst x mod s = 0) + Z.eqb_cps (fst x mod s) 0 + (fun b => + if b then f (fst sxs', cons (fst x / s, snd x) (snd sxs')) - else f (cons x (fst sxs'), snd sxs')) + else f (cons x (fst sxs'), snd sxs'))) end. End split_cps. |