From f932c72dc669d4ae8e152f6a117a03c25e6dbabd Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 29 Apr 2016 15:44:07 -0400 Subject: Moved sign_bit definition to Spec. --- src/Specific/Ed25519.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Specific') 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. { -- cgit v1.2.3