diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-19 12:15:39 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-19 12:15:39 -0400 |
| commit | e2f5be5058052be6da5d079aeda44c7d90328a11 (patch) | |
| tree | 3a56334e307a1500baf1af9592005af836e1f41d | |
| parent | 2f4486861dc86594e0e1fb6b2dc8f32ebba7f651 (diff) | |
Fix build error
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index 12f91759c..9a9ba8149 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -72,9 +72,9 @@ Section WordByWordMontgomery. Local Lemma small_add' : forall n a b, small a -> small b -> small (@add' n a b). Proof. intros; apply Saturated.small_add; auto; try lia. - cbv [uweight]. + (*cbv [uweight]. rewrite !Znat.Nat2Z.inj_succ, !Z.pow_succ_r by lia. - try nia. + try nia.*) Admitted. Local Notation conditional_subtract_cps := (@drop_high_cps R_numlimbs). (*Axiom conditional_subtract_cps : T (S R_numlimbs) -> forall {cpsT}, (T R_numlimbs -> cpsT) -> cpsT *)(* computes [arg - N] if [R <= arg], and drops high bit *) |