diff options
Diffstat (limited to 'src/Fancy/Montgomery256.v')
| -rw-r--r-- | src/Fancy/Montgomery256.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Fancy/Montgomery256.v b/src/Fancy/Montgomery256.v index e5f9c5072..19415ad03 100644 --- a/src/Fancy/Montgomery256.v +++ b/src/Fancy/Montgomery256.v @@ -7,7 +7,8 @@ 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.Arithmetic. (* For the MontgomeryReduction Module *) +Require Import Crypto.PushButtonSynthesis.MontgomeryReduction. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -140,7 +141,7 @@ Module Montgomery256. { cbn. repeat match goal with | _ => apply Compilers.expr.WfLetIn - | _ => progress wf_subgoal + | _ => progress wf_subgoal | _ => econstructor end. } { cbn. cbv [N' N]. @@ -317,4 +318,4 @@ preconditions. *) (* Check Montgomery256.prod_montred256_correct. Print Assumptions Montgomery256.prod_montred256_correct. -*)
\ No newline at end of file +*) |