Changed name of Encoding to CanonicalEncoding, and changed notation to match.

3 files changed, 4 insertions, 4 deletions

diff --git a/src/Encoding/EncodingTheorems.v b/src/Encoding/EncodingTheorems.v
index f53ad0319..52ac91ada 100644
--- a/src/Encoding/EncodingTheorems.v
+++ b/src/Encoding/EncodingTheorems.v
@@ -1,7 +1,7 @@
 Require Import Crypto.Spec.Encoding.
 
 Section EncodingTheorems.
-  Context {A B : Type} {E : encoding of A as B}.
+  Context {A B : Type} {E : canonical encoding of A as B}.
   
   Lemma encoding_inj : forall x y, enc x = enc y -> x = y.
   Proof.
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.
diff --git a/src/Encoding/PointEncodingTheorems.v b/src/Encoding/PointEncodingTheorems.v
index 7bf207c88..2713bd063 100644
--- a/src/Encoding/PointEncodingTheorems.v
+++ b/src/Encoding/PointEncodingTheorems.v
@@ -1,7 +1,7 @@
 
 Section PointEncoding.
   Context {prm: CompleteEdwardsCurve.TwistedEdwardsParams} {sz : nat}
-   {FqEncoding : encoding of ModularArithmetic.F (CompleteEdwardsCurve.q) as Word.word sz}
+   {FqEncoding : canonical encoding of ModularArithmetic.F (CompleteEdwardsCurve.q) as Word.word sz}
    {q_5mod8 : (CompleteEdwardsCurve.q mod 8 = 5)%Z}
    {sqrt_minus1_valid : (@ZToField CompleteEdwardsCurve.q 2 ^ BinInt.Z.to_N (CompleteEdwardsCurve.q / 4)) ^ 2 = opp 1}.
   Existing Instance CompleteEdwardsCurve.prime_q.
@@ -180,7 +180,7 @@ Proof.
     rewrite onCurve_p in Heqb; auto.
 Qed.
 
-Instance point_encoding : encoding of point as (word (S sz)) := {
+Instance point_encoding : canonical encoding of point as (word (S sz)) := {
   enc := point_enc;
   dec := point_dec;
   encoding_valid := point_encoding_valid