diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-06-27 09:16:12 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-06-27 09:22:14 -0400 |
| commit | 163567bf8784708bc5e1b58c50450b8d5d5ab106 (patch) | |
| tree | 3a358f40495fedd4a87438f98ba14cc4e212604d /src/Arithmetic/MontgomeryReduction | |
| parent | 718c852b530aab5c505db7d7ab0fb8d8edd6e10a (diff) | |
proved eval_mod and eval_div (last remaining eval_ admits in Saturated)
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction')
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index c68bde2e0..a55f9cffe 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -24,7 +24,7 @@ Section WordByWordMontgomery. Local Notation small_scmul := (fun n a v _ _ _ => @small_scmul r (Zorder.Zgt_pos_0 _) n a v). Local Notation eval_join0 := (@eval_zero (Z.pos r) (Zorder.Zgt_pos_0 _)). Local Notation eval_div := (@eval_div (Z.pos r) (Zorder.Zgt_pos_0 _)). - Local Notation eval_mod := (@eval_mod (Z.pos r) (Zorder.Zgt_pos_0 _)). + Local Notation eval_mod := (@eval_mod (Z.pos r)). Local Notation small_div := (@small_div (Z.pos r) (Zorder.Zgt_pos_0 _)). Local Notation eval_scmul := (fun n a v smallv abound vbound => @eval_scmul (Z.pos r) (Zorder.Zgt_pos_0 _) n a v smallv abound). Local Notation eval_addT := (@eval_add_same (Z.pos r) (Zorder.Zgt_pos_0 _)). |