Fix changes in naming in SpecificGen

1 files changed, 117 insertions, 117 deletions

diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4
index 6c25c91ca..0ad1a423a 100644
--- a/src/SpecificGen/GFtemplate3mod4
+++ b/src/SpecificGen/GFtemplate3mod4
@@ -25,15 +25,15 @@ Lemma prime_modulus : prime modulus. Admitted.
 Definition freeze_input_bound := {{{w}}}%Z.
 Definition int_width := {{{w}}}%Z.
 
-Instance params : PseudoMersenneBaseParams modulus.
+Instance params{{{k}}}{{{c}}}_{{{w}}} : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus {{{n}}}%nat {{{k}}}.
 Defined.
 
-Definition length_fe := Eval compute in length limb_widths.
-Definition fe := Eval compute in (tuple Z length_fe).
+Definition length_fe{{{k}}}{{{c}}}_{{{w}}} := Eval compute in length limb_widths.
+Definition fe{{{k}}}{{{c}}}_{{{w}}} := Eval compute in (tuple Z length_fe{{{k}}}{{{c}}}_{{{w}}}).
 
-Definition mul2modulus : fe :=
-  Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params)).
+Definition mul2modulus : fe{{{k}}}{{{c}}}_{{{w}}} :=
+  Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params{{{k}}}{{{c}}}_{{{w}}})).
 
 Instance subCoeff : SubtractionCoefficient.
   apply Build_SubtractionCoefficient with (coeff := mul2modulus).
@@ -150,24 +150,24 @@ Proof.
   reflexivity.
 Qed.
 
-Definition app_n {T} (f : fe) (P : fe -> T) : T.
+Definition app_n {T} (f : fe{{{k}}}{{{c}}}_{{{w}}}) (P : fe{{{k}}}{{{c}}}_{{{w}}} -> T) : T.
 Proof.
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   set (f0 := f).
   repeat (let g := fresh "g" in destruct f as [f g]).
   apply P.
   apply f0.
 Defined.
 
-Definition app_n_correct {T} f (P : fe -> T) : app_n f P = P f.
+Definition app_n_correct {T} f (P : fe{{{k}}}{{{c}}}_{{{w}}} -> T) : app_n f P = P f.
 Proof.
   intros.
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
   reflexivity.
 Qed.
 
-Definition appify2 {T} (op : fe -> fe -> T) (f g : fe) :=
+Definition appify2 {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :=
   app_n f (fun f0 => (app_n g (fun g0 => op f0 g0))).
 
 Lemma appify2_correct : forall {T} op f g, @appify2 T op f g = op f g.
@@ -176,102 +176,102 @@ Proof.
   etransitivity; apply app_n_correct.
 Qed.
 
-Definition uncurry_unop_fe {T} (op : fe -> T)
-  := Eval compute in Tuple.uncurry (n:=length_fe) op.
-Definition curry_unop_fe {T} op : fe -> T
-  := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe) op).
-Definition uncurry_binop_fe {T} (op : fe -> fe -> T)
-  := Eval compute in uncurry_unop_fe (fun f => uncurry_unop_fe (op f)).
-Definition curry_binop_fe {T} op : fe -> fe -> T
-  := Eval compute in appify2 (fun f => curry_unop_fe (curry_unop_fe op f)).
+Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T)
+  := Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op.
+Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T
+  := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op).
+Definition uncurry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T)
+  := Eval compute in uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun f => uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (op f)).
+Definition curry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T
+  := Eval compute in appify2 (fun f => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op f)).
 
 Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
   := Eval compute in Tuple.uncurry (n:=length wire_widths) op.
 Definition curry_unop_wire_digits {T} op : wire_digits -> T
   := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
 
-Definition add_sig (f g : fe) :
-  { fg : fe | fg = add_opt f g}.
+Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}.
 Proof.
   eexists.
-  rewrite <-(@appify2_correct fe).
+  rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}).
   cbv.
   reflexivity.
 Defined.
 
-Definition add (f g : fe) : fe :=
+Definition add (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
   Eval cbv beta iota delta [proj1_sig add_sig] in
   proj1_sig (add_sig f g).
 
-Definition add_correct (f g : fe)
+Definition add_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}})
   : add f g = add_opt f g :=
   Eval cbv beta iota delta [proj1_sig add_sig] in
   proj2_sig (add_sig f g).
 
-Definition carry_add_sig (f g : fe) :
-  { fg : fe | fg = carry_add_opt f g}.
+Definition carry_add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_add_opt f g}.
 Proof.
   eexists.
-  rewrite <-(@appify2_correct fe).
+  rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}).
   cbv.
   autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv.
   autorewrite with zsimplify_Z_to_pos; cbv.
   reflexivity.
 Defined.
 
-Definition carry_add (f g : fe) : fe :=
+Definition carry_add (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
   Eval cbv beta iota delta [proj1_sig carry_add_sig] in
   proj1_sig (carry_add_sig f g).
 
-Definition carry_add_correct (f g : fe)
+Definition carry_add_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}})
   : carry_add f g = carry_add_opt f g :=
   Eval cbv beta iota delta [proj1_sig carry_add_sig] in
   proj2_sig (carry_add_sig f g).
 
-Definition sub_sig (f g : fe) :
-  { fg : fe | fg = sub_opt f g}.
+Definition sub_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = sub_opt f g}.
 Proof.
   eexists.
-  rewrite <-(@appify2_correct fe).
+  rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}).
   cbv.
   reflexivity.
 Defined.
 
-Definition sub (f g : fe) : fe :=
+Definition sub (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
   Eval cbv beta iota delta [proj1_sig sub_sig] in
   proj1_sig (sub_sig f g).
 
-Definition sub_correct (f g : fe)
+Definition sub_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}})
   : sub f g = sub_opt f g :=
   Eval cbv beta iota delta [proj1_sig sub_sig] in
   proj2_sig (sub_sig f g).
 
-Definition carry_sub_sig (f g : fe) :
-  { fg : fe | fg = carry_sub_opt f g}.
+Definition carry_sub_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_sub_opt f g}.
 Proof.
   eexists.
-  rewrite <-(@appify2_correct fe).
+  rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}).
   cbv.
   autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv.
   autorewrite with zsimplify_Z_to_pos; cbv.
   reflexivity.
 Defined.
 
-Definition carry_sub (f g : fe) : fe :=
+Definition carry_sub (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
   Eval cbv beta iota delta [proj1_sig carry_sub_sig] in
   proj1_sig (carry_sub_sig f g).
 
-Definition carry_sub_correct (f g : fe)
+Definition carry_sub_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}})
   : carry_sub f g = carry_sub_opt f g :=
   Eval cbv beta iota delta [proj1_sig carry_sub_sig] in
   proj2_sig (carry_sub_sig f g).
 
 (* For multiplication, we add another layer of definition so that we can
    rewrite under the [let] binders. *)
-Definition mul_simpl_sig (f g : fe) :
-  { fg : fe | fg = carry_mul_opt k_ c_ f g}.
+Definition mul_simpl_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_mul_opt k_ c_ f g}.
 Proof.
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   eexists.
   cbv. (* N.B. The slow part of this is computing with [Z_div_opt].
@@ -282,45 +282,45 @@ Proof.
   reflexivity.
 Defined.
 
-Definition mul_simpl (f g : fe) : fe :=
+Definition mul_simpl (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
   Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in
   let '{{{enum f}}} := f in
   let '{{{enum g}}} := g in
   proj1_sig (mul_simpl_sig {{{enum f}}}
                            {{{enum g}}}).
 
-Definition mul_simpl_correct (f g : fe)
+Definition mul_simpl_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}})
   : mul_simpl f g = carry_mul_opt k_ c_ f g.
 Proof.
   pose proof (proj2_sig (mul_simpl_sig f g)).
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Qed.
 
-Definition mul_sig (f g : fe) :
-  { fg : fe | fg = carry_mul_opt k_ c_ f g}.
+Definition mul_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = carry_mul_opt k_ c_ f g}.
 Proof.
   eexists.
   rewrite <-mul_simpl_correct.
-  rewrite <-(@appify2_correct fe).
+  rewrite <-(@appify2_correct fe{{{k}}}{{{c}}}_{{{w}}}).
   cbv.
   autorewrite with zsimplify_fast zsimplify_Z_to_pos; cbv.
   autorewrite with zsimplify_Z_to_pos; cbv.
   reflexivity.
 Defined.
 
-Definition mul (f g : fe) : fe :=
+Definition mul (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
   Eval cbv beta iota delta [proj1_sig mul_sig] in
   proj1_sig (mul_sig f g).
 
-Definition mul_correct (f g : fe)
+Definition mul_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}})
   : mul f g = carry_mul_opt k_ c_ f g :=
   Eval cbv beta iota delta [proj1_sig add_sig] in
   proj2_sig (mul_sig f g).
 
-Definition opp_sig (f : fe) :
-  { g : fe | g = opp_opt f }.
+Definition opp_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = opp_opt f }.
 Proof.
   eexists.
   cbv [opp_opt].
@@ -330,15 +330,15 @@ Proof.
   reflexivity.
 Defined.
 
-Definition opp (f : fe) : fe
+Definition opp (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}}
   := Eval cbv beta iota delta [proj1_sig opp_sig] in proj1_sig (opp_sig f).
 
-Definition opp_correct (f : fe)
+Definition opp_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
   : opp f = opp_opt f
   := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (opp_sig f).
 
-Definition carry_opp_sig (f : fe) :
-  { g : fe | g = carry_opp_opt f }.
+Definition carry_opp_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = carry_opp_opt f }.
 Proof.
   eexists.
   cbv [carry_opp_opt].
@@ -348,16 +348,16 @@ Proof.
   reflexivity.
 Defined.
 
-Definition carry_opp (f : fe) : fe
+Definition carry_opp (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}}
   := Eval cbv beta iota delta [proj1_sig carry_opp_sig] in proj1_sig (carry_opp_sig f).
 
-Definition carry_opp_correct (f : fe)
+Definition carry_opp_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
   : carry_opp f = carry_opp_opt f
   := Eval cbv beta iota delta [proj2_sig add_sig] in proj2_sig (carry_opp_sig f).
 
-Definition pow (f : fe) chain := fold_chain_opt one_ mul chain [f].
+Definition pow (f : fe{{{k}}}{{{c}}}_{{{w}}}) chain := fold_chain_opt one_ mul chain [f].
 
-Lemma pow_correct (f : fe) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain.
+Lemma pow_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) : forall chain, pow f chain = pow_opt k_ c_ one_ f chain.
 Proof.
   cbv [pow pow_opt]; intros.
   rewrite !fold_chain_opt_correct.
@@ -365,8 +365,8 @@ Proof.
   intros; subst; apply mul_correct.
 Qed.
 
-Definition inv_sig (f : fe) :
-  { g : fe | g = inv_opt k_ c_ one_ f }.
+Definition inv_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { g : fe{{{k}}}{{{c}}}_{{{w}}} | g = inv_opt k_ c_ one_ f }.
 Proof.
   eexists; cbv [inv_opt].
   rewrite <-pow_correct.
@@ -374,10 +374,10 @@ Proof.
   reflexivity.
 Defined.
 
-Definition inv (f : fe) : fe
+Definition inv (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}}
   := Eval cbv beta iota delta [proj1_sig inv_sig] in proj1_sig (inv_sig f).
 
-Definition inv_correct (f : fe)
+Definition inv_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
   : inv f = inv_opt k_ c_ one_ f
   := Eval cbv beta iota delta [proj2_sig inv_sig] in proj2_sig (inv_sig f).
 
@@ -388,12 +388,12 @@ Import Morphisms.
 Local Existing Instance prime_modulus.
 
 Lemma field_and_homomorphisms
-  : @field fe eq zero_ one_ opp add sub mul inv div
+  : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div
     /\ @Ring.is_homomorphism
          (F modulus) Logic.eq F.one F.add F.mul
-         fe eq one_ add mul encode
+         fe{{{k}}}{{{c}}}_{{{w}}} eq one_ add mul encode
     /\ @Ring.is_homomorphism
-         fe eq one_ add mul
+         fe{{{k}}}{{{c}}}_{{{w}}} eq one_ add mul
          (F modulus) Logic.eq F.one F.add F.mul
          decode.
 Proof.
@@ -411,15 +411,15 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition field{{{k}}}{{{c}}} : @field fe eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
+Definition field{{{k}}}{{{c}}} : @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 eq zero_ one_ carry_opp carry_add carry_sub mul inv div
+  : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div
     /\ @Ring.is_homomorphism
          (F modulus) Logic.eq F.one F.add F.mul
-         fe eq one_ carry_add mul encode
+         fe{{{k}}}{{{c}}}_{{{w}}} eq one_ carry_add mul encode
     /\ @Ring.is_homomorphism
-         fe eq one_ carry_add mul
+         fe{{{k}}}{{{c}}}_{{{w}}} eq one_ carry_add mul
          (F modulus) Logic.eq F.one F.add F.mul
          decode.
 Proof.
@@ -437,29 +437,29 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition carry_field : @field fe eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
+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.
 
 Lemma homomorphism_F_encode
-  : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one add mul 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
-  : @Ring.is_homomorphism fe eq one add mul (F modulus) Logic.eq F.one F.add F.mul 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
-  : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe eq one carry_add mul 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
-  : @Ring.is_homomorphism fe eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul 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.
 
-Definition ge_modulus_sig (f : fe) :
+Definition ge_modulus_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
   { b : Z | b = ge_modulus_opt (to_list {{{n}}} f) }.
 Proof.
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   eexists; cbv [ge_modulus_opt].
   rewrite !modulus_digits_subst.
@@ -467,24 +467,24 @@ Proof.
   reflexivity.
 Defined.
 
-Definition ge_modulus (f : fe) : Z :=
+Definition ge_modulus (f : fe{{{k}}}{{{c}}}_{{{w}}}) : Z :=
   Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in
     let '{{{enum f}}} := f in
     proj1_sig (ge_modulus_sig {{{enum f}}}).
 
-Definition ge_modulus_correct (f : fe) :
+Definition ge_modulus_correct (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
   ge_modulus f = ge_modulus_opt (to_list {{{n}}} f).
 Proof.
   pose proof (proj2_sig (ge_modulus_sig f)).
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
 
-Definition freeze_sig (f : fe) :
-  { f' : fe | f' = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)) }.
+Definition freeze_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)) }.
 Proof.
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   eexists; cbv [freeze_opt int_width].
   cbv [to_list to_list'].
@@ -499,38 +499,38 @@ Proof.
   reflexivity.
 Defined.
 
-Definition freeze (f : fe) : fe :=
+Definition freeze (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}} :=
   Eval cbv beta iota delta [proj1_sig freeze_sig] in
     let '{{{enum f}}} := f in
     proj1_sig (freeze_sig {{{enum f}}}).
 
-Definition freeze_correct (f : fe)
+Definition freeze_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
   : freeze f = from_list_default 0 {{{n}}} (freeze_opt (int_width := int_width) c_ (to_list {{{n}}} f)).
 Proof.
   pose proof (proj2_sig (freeze_sig f)).
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
 
-Definition fieldwiseb_sig (f g : fe) :
+Definition fieldwiseb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
   { b | b = @fieldwiseb Z Z {{{n}}} Z.eqb f g }.
 Proof.
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   eexists.
   cbv.
   reflexivity.
 Defined.
 
-Definition fieldwiseb (f g : fe) : bool
+Definition fieldwiseb (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : bool
   := Eval cbv beta iota delta [proj1_sig fieldwiseb_sig] in
       let '{{{enum f}}} := f in
       let '{{{enum g}}} := g in
       proj1_sig (fieldwiseb_sig {{{enum f}}}
                                 {{{enum g}}}).
 
-Lemma fieldwiseb_correct (f g : fe)
+Lemma fieldwiseb_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}})
   : fieldwiseb f g = @Tuple.fieldwiseb Z Z {{{n}}} Z.eqb f g.
 Proof.
   set (f' := f); set (g' := g).
@@ -538,11 +538,11 @@ Proof.
   exact (proj2_sig (fieldwiseb_sig f' g')).
 Qed.
 
-Definition eqb_sig (f g : fe) :
+Definition eqb_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
   { b | b = eqb int_width f g }.
 Proof.
   cbv [eqb].
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   eexists.
   cbv [ModularBaseSystem.freeze int_width].
@@ -553,14 +553,14 @@ Proof.
   reflexivity.
 Defined.
 
-Definition eqb (f g : fe) : bool
+Definition eqb (f g : fe{{{k}}}{{{c}}}_{{{w}}}) : bool
   := Eval cbv beta iota delta [proj1_sig eqb_sig] in
       let '{{{enum f}}} := f in
       let '{{{enum g}}} := g in
       proj1_sig (eqb_sig {{{enum f}}}
                          {{{enum g}}}).
 
-Lemma eqb_correct (f g : fe)
+Lemma eqb_correct (f g : fe{{{k}}}{{{c}}}_{{{w}}})
   : eqb f g = ModularBaseSystem.eqb int_width f g.
 Proof.
   set (f' := f); set (g' := g).
@@ -568,8 +568,8 @@ Proof.
   exact (proj2_sig (eqb_sig f' g')).
 Qed.
 
-Definition sqrt_sig (f : fe) :
-  { f' : fe | f' = sqrt_3mod4_opt k_ c_ one_ f}.
+Definition sqrt_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { f' : fe{{{k}}}{{{c}}}_{{{w}}} | f' = sqrt_3mod4_opt k_ c_ one_ f}.
 Proof.
   eexists.
   cbv [sqrt_3mod4_opt int_width].
@@ -577,17 +577,17 @@ Proof.
   reflexivity.
 Defined.
 
-Definition sqrt (f : fe) : fe
+Definition sqrt (f : fe{{{k}}}{{{c}}}_{{{w}}}) : fe{{{k}}}{{{c}}}_{{{w}}}
   := Eval cbv beta iota delta [proj1_sig sqrt_sig] in proj1_sig (sqrt_sig f).
 
-Definition sqrt_correct (f : fe)
+Definition sqrt_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
   : sqrt f = sqrt_3mod4_opt k_ c_ one_ f
   := Eval cbv beta iota delta [proj2_sig sqrt_sig] in proj2_sig (sqrt_sig f).
 
-Definition pack_simpl_sig (f : fe) :
-  { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }.
+Definition pack_simpl_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { f' | f' = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }.
 Proof.
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   eexists.
   cbv [pack_opt].
@@ -598,22 +598,22 @@ Proof.
   reflexivity.
 Defined.
 
-Definition pack_simpl (f : fe) :=
+Definition pack_simpl (f : fe{{{k}}}{{{c}}}_{{{w}}}) :=
   Eval cbv beta iota delta [proj1_sig pack_simpl_sig] in
     let '{{{enum f}}} := f in
     proj1_sig (pack_simpl_sig {{{enum f}}}).
 
-Definition pack_simpl_correct (f : fe)
-  : pack_simpl f = pack_opt params wire_widths_nonneg bits_eq f.
+Definition pack_simpl_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
+  : pack_simpl f = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f.
 Proof.
   pose proof (proj2_sig (pack_simpl_sig f)).
-  cbv [fe] in *.
+  cbv [fe{{{k}}}{{{c}}}_{{{w}}}] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Qed.
 
-Definition pack_sig (f : fe) :
-  { f' | f' = pack_opt params wire_widths_nonneg bits_eq f }.
+Definition pack_sig (f : fe{{{k}}}{{{c}}}_{{{w}}}) :
+  { f' | f' = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }.
 Proof.
   eexists.
   rewrite <-pack_simpl_correct.
@@ -622,15 +622,15 @@ Proof.
   reflexivity.
 Defined.
 
-Definition pack (f : fe) : wire_digits :=
+Definition pack (f : fe{{{k}}}{{{c}}}_{{{w}}}) : wire_digits :=
   Eval cbv beta iota delta [proj1_sig pack_sig] in proj1_sig (pack_sig f).
 
-Definition pack_correct (f : fe)
-  : pack f = pack_opt params wire_widths_nonneg bits_eq f
+Definition pack_correct (f : fe{{{k}}}{{{c}}}_{{{w}}})
+  : pack f = pack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f
   := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (pack_sig f).
 
 Definition unpack_simpl_sig (f : wire_digits) :
-  { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }.
+  { f' | f' = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }.
 Proof.
   cbv [wire_digits] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
@@ -644,13 +644,13 @@ Proof.
   reflexivity.
 Defined.
 
-Definition unpack_simpl (f : wire_digits) : fe :=
+Definition unpack_simpl (f : wire_digits) : fe{{{k}}}{{{c}}}_{{{w}}} :=
   Eval cbv beta iota delta [proj1_sig unpack_simpl_sig] in
     let '{{{enumw f}}} := f in
     proj1_sig (unpack_simpl_sig {{{enumw f}}}).
 
 Definition unpack_simpl_correct (f : wire_digits)
-  : unpack_simpl f = unpack_opt params wire_widths_nonneg bits_eq f.
+  : unpack_simpl f = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f.
 Proof.
   pose proof (proj2_sig (unpack_simpl_sig f)).
   cbv [wire_digits] in *.
@@ -659,18 +659,18 @@ Proof.
 Qed.
 
 Definition unpack_sig (f : wire_digits) :
-  { f' | f' = unpack_opt params wire_widths_nonneg bits_eq f }.
+  { f' | f' = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f }.
 Proof.
   eexists.
   rewrite <-unpack_simpl_correct.
-  rewrite <-(@app_n2_correct fe).
+  rewrite <-(@app_n2_correct fe{{{k}}}{{{c}}}_{{{w}}}).
   cbv.
   reflexivity.
 Defined.
 
-Definition unpack (f : wire_digits) : fe :=
+Definition unpack (f : wire_digits) : fe{{{k}}}{{{c}}}_{{{w}}} :=
   Eval cbv beta iota delta [proj1_sig unpack_sig] in proj1_sig (unpack_sig f).
 
 Definition unpack_correct (f : wire_digits)
-  : unpack f = unpack_opt params wire_widths_nonneg bits_eq f
+  : unpack f = unpack_opt params{{{k}}}{{{c}}}_{{{w}}} wire_widths_nonneg bits_eq f
   := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f).