before changing SRep from N to F l

3 files changed, 7 insertions, 15 deletions

diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 99f0766e0..a0e5e9da7 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -46,9 +46,9 @@ End EdDSAParams.
 
 Section EdDSA.
   Context {prm:EdDSAParams}.
-  Existing Instance E.
-  Existing Instance PointEncoding.
-  Existing Instance FlEncoding.
+  Global Existing Instance E.
+  Global Existing Instance PointEncoding.
+  Global Existing Instance FlEncoding.
   Existing Class le.
   Existing Instance n_le_b.
 
diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v
index d6f6bcb3c..acd2bedbd 100644
--- a/src/Spec/ModularWordEncoding.v
+++ b/src/Spec/ModularWordEncoding.v
@@ -28,7 +28,7 @@ Section ModularWordEncoding.
     | Word.WS b _ w' => b
   end.
 
-  Instance modular_word_encoding : canonical encoding of F m as word sz := {
+  Global Instance modular_word_encoding : canonical encoding of F m as word sz := {
     enc := Fm_enc;
     dec := Fm_dec;
     encoding_valid :=
diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v
index f4634f52f..29e359baa 100644
--- a/src/Spec/PointEncoding.v
+++ b/src/Spec/PointEncoding.v
@@ -20,7 +20,6 @@ Section PointEncoding.
    {FqEncoding : canonical encoding of (F q) as (Word.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.
 
   Definition point_enc (p : E.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in
     Word.WS (sign_bit x) (enc y).
@@ -29,19 +28,12 @@ Section PointEncoding.
     {point_dec : Word.word (S sz) -> option E.point
                | forall w x, point_dec w = Some x -> (point_enc x = w)
                } := @PointEncodingPre.point_dec _ _ _ sign_bit.
-
   Definition point_dec := Eval hnf in (proj1_sig point_dec_with_spec).
 
-   Definition point_encoding_valid : forall p : E.point, point_dec (point_enc p) = Some p :=
-     @PointEncodingPre.point_encoding_valid _ _ q_5mod8 sqrt_minus1_valid _ _ sign_bit_zero sign_bit_opp.
-
-   Definition point_encoding_canonical : forall x_enc x, point_dec x_enc = Some x -> point_enc x = x_enc :=
-     PointEncodingPre.point_encoding_canonical.
-
-  Instance point_encoding : canonical encoding of E.point as (Word.word (S sz)) := {
+  Global Instance point_encoding : canonical encoding of E.point as (Word.word (S sz)) := {
     enc := point_enc;
     dec := point_dec;
-    encoding_valid := point_encoding_valid;
-    encoding_canonical := point_encoding_canonical
+    encoding_valid := @PointEncodingPre.point_encoding_valid _ _ q_5mod8 sqrt_minus1_valid _ _ sign_bit_zero sign_bit_opp;
+    encoding_canonical := PointEncodingPre.point_encoding_canonical
   }.
 End PointEncoding.
\ No newline at end of file