diff options
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF1305.v | 2 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 2 |
2 files changed, 2 insertions, 2 deletions
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. |