From 4a2c65e57a107545654c2ae815efd734ca7d8321 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 15 Jun 2016 18:00:35 -0400 Subject: PseudoMersenneBaseRep.mul now carries by default (made possible by strictly base-length digit vectors) --- src/Specific/GF1305.v | 2 +- src/Specific/GF25519.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index b004a60d1..31dee21f3 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -45,7 +45,7 @@ Lemma GF1305Base26_mul_reduce_formula : -> rep ls (f*g)%F}. Proof. eexists; intros ? ? Hf Hg. - pose proof (carry_mul_opt_correct k_ c_ (eq_refl k) (eq_refl c_) [0;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg. + pose proof (carry_mul_opt_rep k_ c_ (eq_refl k) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg. compute_formula. Defined. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 68278ce4c..37e0c08db 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -47,7 +47,7 @@ Lemma GF25519Base25Point5_mul_reduce_formula : -> rep ls (f*g)%F}. Proof. eexists; intros ? ? Hf Hg. - pose proof (carry_mul_opt_correct k_ c_ (eq_refl k_) (eq_refl c_) [0;9;8;7;6;5;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg. + pose proof (carry_mul_opt_rep k_ c_ (eq_refl k_) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg. compute_formula. Time Defined. -- cgit v1.2.3