diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-29 15:44:07 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-29 15:44:07 -0400 |
| commit | f932c72dc669d4ae8e152f6a117a03c25e6dbabd (patch) | |
| tree | 5765e60cd039634ea59b2f9b1f0c3120247ec0ff /src/Specific | |
| parent | a82770a13960d214a76265620096d0f266ca00cd (diff) | |
Moved sign_bit definition to Spec.
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/Ed25519.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 5107c1468..fa1c44d08 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -359,7 +359,7 @@ Proof. reflexivity. } Unfocus. - cbv iota beta delta [point_dec_coordinates ModularWordEncodingTheorems.sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. + cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. etransitivity. Focus 2. { |