[F] has its own module now

[ZToField] -> [F.of_Z]
[FieldToZ] -> [F.to_Z]
[Zmod.lem] -> [F.lem]

1 files changed, 6 insertions, 6 deletions

diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v
index aea22f4f5..fbd9238c1 100644
--- a/src/Encoding/ModularWordEncodingPre.v
+++ b/src/Encoding/ModularWordEncodingPre.v
@@ -11,23 +11,23 @@ Local Open Scope nat_scope.
 Section ModularWordEncodingPre.
   Context {m : Z} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}.
 
-  Let Fm_enc (x : F m) : word sz := NToWord sz (Z.to_N (FieldToZ x)).
+  Let Fm_enc (x : F m) : word sz := NToWord sz (Z.to_N (F.to_Z x)).
 
   Let Fm_dec (x_ : word sz) : option (F m) :=
     let z := Z.of_N (wordToN (x_)) in
     if Z_lt_dec z m
-      then Some (ZToField _ z)
+      then Some (F.of_Z m z)
       else None
   .
 
   Lemma Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x.
   Proof.
     unfold Fm_dec, Fm_enc; intros.
-    pose proof (Zmod.FieldToZ_range x m_pos).
+    pose proof (F.to_Z_range x m_pos).
     rewrite wordToN_NToWord_idempotent by (apply bound_check_nat_N;
-     assert (Z.to_nat x < Z.to_nat m) by (apply Z2Nat.inj_lt; omega); omega).
+     assert (Z.to_nat (F.to_Z x) < Z.to_nat m) by (apply Z2Nat.inj_lt; omega); omega).
     rewrite Z2N.id by omega.
-    rewrite Zmod.ZToField_FieldToZ.
+    rewrite F.of_Z_to_Z.
     break_if; auto; omega.
   Qed.
 
@@ -36,7 +36,7 @@ Section ModularWordEncodingPre.
     unfold Fm_dec, Fm_enc; intros ? ? dec_Some.
     break_if; [ | congruence ].
     inversion dec_Some.
-    rewrite Zmod.FieldToZ_ZToField.
+    rewrite F.to_Z_of_Z.
     rewrite Z.mod_small by (pose proof (N2Z.is_nonneg (wordToN w)); try omega).
     rewrite N2Z.id.
     apply NToWord_wordToN.