diff options
Diffstat (limited to 'src/Fancy/Barrett256.v')
| -rw-r--r-- | src/Fancy/Barrett256.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Fancy/Barrett256.v b/src/Fancy/Barrett256.v index 2ee19e6e6..46e8f6f52 100644 --- a/src/Fancy/Barrett256.v +++ b/src/Fancy/Barrett256.v @@ -8,7 +8,7 @@ Require Import Crypto.Fancy.Prod. Require Import Crypto.Fancy.Spec. Require Import Crypto.Language. Import Language.Compilers. Require Import Crypto.LanguageWf. -Require Import Crypto.PushButtonSynthesis. +Require Import Crypto.PushButtonSynthesis.BarrettReduction. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -144,7 +144,7 @@ Module Barrett256. { cbn. repeat match goal with | _ => apply Compilers.expr.WfLetIn - | _ => progress wf_subgoal + | _ => progress wf_subgoal | _ => econstructor end. } { cbn. cbv [muLow M]. @@ -299,7 +299,7 @@ Module Barrett256. repeat match goal with H : context [start_context] |- _ => rewrite <-H end. - + cbv [barrett_red256_alloc barrett_red256_fancy]. repeat step. reflexivity. @@ -399,4 +399,4 @@ Eval cbv beta iota delta [Barrett256.barrett_red256_alloc] in Barrett256.barrett Check Barrett256.prod_barrett_red256_correct. Print Assumptions Barrett256.prod_barrett_red256_correct. (* The equivalence with generated code is admitted as barrett_red256_alloc_equivalent. *) -*)
\ No newline at end of file +*) |