diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-06-15 00:48:34 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-06-15 00:48:34 -0400 |
| commit | 9d55a380b76b791648071e6354353e587132c119 (patch) | |
| tree | 2b92417f3d953c85db08abf092208a7f4240ca2e /src | |
| parent | 129c6b71a2301d56dd1e3ffe798f4609ae1a0bf8 (diff) | |
fix wrong number of limbs for square as well
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/Karatsuba.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/Karatsuba.v b/src/Specific/Karatsuba.v index 01be5a0c4..410e17548 100644 --- a/src/Specific/Karatsuba.v +++ b/src/Specific/Karatsuba.v @@ -251,7 +251,7 @@ Ltac basesystem_partial_evaluation_RHS := Defined. Definition square_sig : - {square : (Z^sz -> Z^sz2)%type | + {square : (Z^sz -> Z^sz)%type | forall a : Z^sz, let eval := Positional.Fdecode (m := m) wt in Positional.Fdecode (m := m) wt (square a) = (eval a * eval a)%F}. |