1 files changed, 4 insertions, 4 deletions
diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v
index 417344b43..aea22f4f5 100644
--- a/src/Encoding/ModularWordEncodingPre.v
+++ b/src/Encoding/ModularWordEncodingPre.v
@@ -16,18 +16,18 @@ Section ModularWordEncodingPre.
   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 (ZToField _ 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 (FieldToZ_range x m_pos).
+    pose proof (Zmod.FieldToZ_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).
     rewrite Z2N.id by omega.
-    rewrite ZToField_idempotent.
+    rewrite Zmod.ZToField_FieldToZ.
     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 FieldToZ_ZToField.
+    rewrite Zmod.FieldToZ_ZToField.
     rewrite Z.mod_small by (pose proof (N2Z.is_nonneg (wordToN w)); try omega).
     rewrite N2Z.id.
     apply NToWord_wordToN.