aboutsummaryrefslogtreecommitdiff
path: root/src/Encoding/PointEncodingPre.v
diff options
context:
space:
mode:
authorGravatar jadep <jade.philipoom@gmail.com>2016-04-29 18:27:26 -0400
committerGravatar jadep <jade.philipoom@gmail.com>2016-04-29 18:27:26 -0400
commit728b2f95dc83329c58aef7624283cb945c77b919 (patch)
tree519e2067b86022405b89287c687977804beacba5 /src/Encoding/PointEncodingPre.v
parent44c3f52e7d431b4aa5de8e8679155ea2bed9d31c (diff)
Changed name of Encoding to CanonicalEncoding, and changed notation to match.
Diffstat (limited to 'src/Encoding/PointEncodingPre.v')
-rw-r--r--src/Encoding/PointEncodingPre.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v
index e023da0ea..73ced869b 100644
--- a/src/Encoding/PointEncodingPre.v
+++ b/src/Encoding/PointEncodingPre.v
@@ -17,7 +17,7 @@ Section PointEncoding.
Context {prm: TwistedEdwardsParams} {sz : nat} {sz_nonzero : (0 < sz)%nat}
{bound_check : (Z.to_nat q < 2 ^ sz)%nat} {q_5mod8 : (q mod 8 = 5)%Z}
{sqrt_minus1_valid : (@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1}
- {FqEncoding : encoding of (F q) as (word sz)}
+ {FqEncoding : canonical encoding of (F q) as (word sz)}
{sign_bit : F q -> bool} {sign_bit_zero : sign_bit 0 = false}
{sign_bit_opp : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x)}.
Existing Instance prime_q.