Update field names in SpecificGen

1 files changed, 6 insertions, 6 deletions

diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4
index ccee86d1a..d255befeb 100644
--- a/src/SpecificGen/GFtemplate3mod4
+++ b/src/SpecificGen/GFtemplate3mod4
@@ -420,7 +420,7 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition field{{{k}}}{{{c}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
+Definition field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
 
 Lemma carry_field_and_homomorphisms
   : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div
@@ -446,22 +446,22 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition carry_field : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
+Definition carry_field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
 
-Lemma homomorphism_F_encode
+Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul encode.
 Proof. apply field_and_homomorphisms. Qed.
 
-Lemma homomorphism_F_decode
+Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_decode
   : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply field_and_homomorphisms. Qed.
 
 
-Lemma homomorphism_carry_F_encode
+Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul encode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
-Lemma homomorphism_carry_F_decode
+Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_decode
   : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply carry_field_and_homomorphisms. Qed.