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