Remove dead code for renaming binders

After     | File Name                                      | Before    || Change    | % Change
----------------------------------------------------------------------------------------------
19m16.05s | Total                                          | 21m25.28s || -2m09.23s | -10.05%
----------------------------------------------------------------------------------------------
4m01.34s  | Specific/X25519/C64/ladderstep                 | 4m59.49s  || -0m58.15s | -19.41%
2m48.52s  | Specific/solinas32_2e255m765_13limbs/femul     | 3m12.95s  || -0m24.42s | -12.66%
2m23.70s  | Specific/solinas32_2e255m765_12limbs/femul     | 2m44.11s  || -0m20.41s | -12.43%
3m09.62s  | Specific/NISTP256/AMD64/femul                  | 3m22.52s  || -0m12.90s | -6.36%
0m36.32s  | Specific/X25519/C64/femul                      | 0m39.50s  || -0m03.17s | -8.05%
0m30.13s  | Specific/X25519/C64/fesquare                   | 0m32.24s  || -0m02.11s | -6.54%
0m35.40s  | Specific/NISTP256/AMD64/feadd                  | 0m37.21s  || -0m01.81s | -4.86%
0m31.50s  | Specific/X25519/C64/freeze                     | 0m33.24s  || -0m01.74s | -5.23%
0m24.99s  | Specific/X25519/C64/fecarry                    | 0m26.31s  || -0m01.32s | -5.01%
0m22.65s  | Specific/X25519/C64/fesub                      | 0m23.72s  || -0m01.07s | -4.51%
0m45.75s  | Specific/solinas32_2e255m765_13limbs/Synthesis | 0m45.58s  || +0m00.17s | +0.37%
0m39.59s  | Specific/NISTP256/AMD64/fesub                  | 0m40.09s  || -0m00.50s | -1.24%
0m36.92s  | Specific/solinas32_2e255m765_12limbs/Synthesis | 0m36.64s  || +0m00.28s | +0.76%
0m28.51s  | Specific/NISTP256/AMD64/feopp                  | 0m29.46s  || -0m00.94s | -3.22%
0m25.50s  | Specific/NISTP256/AMD64/fenz                   | 0m26.41s  || -0m00.91s | -3.44%
0m20.93s  | Specific/X25519/C64/feadd                      | 0m21.41s  || -0m00.48s | -2.24%
0m12.55s  | Specific/NISTP256/AMD64/Synthesis              | 0m12.54s  || +0m00.01s | +0.07%
0m10.37s  | Specific/X25519/C64/Synthesis                  | 0m10.30s  || +0m00.06s | +0.67%
0m07.18s  | Compilers/Z/Bounds/Pipeline/Definition         | 0m07.22s  || -0m00.04s | -0.55%
0m01.72s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics  | 0m01.58s  || +0m00.13s | +8.86%
0m01.67s  | Specific/Framework/SynthesisFramework          | 0m01.72s  || -0m00.05s | -2.90%
0m01.19s  | Compilers/Z/Bounds/Pipeline                    | 0m01.04s  || +0m00.14s | +14.42%

2 files changed, 4 insertions, 18 deletions

diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index e5503511d..7d9061cad 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -81,7 +81,6 @@ Record PipelineOptions :=
   {
     anf            : with_default bool false;
     adc_fusion     : with_default bool true;
-    rename_binders : with_default bool false;
   }.
 Definition default_PipelineOptions := {| anf := _ |}.
 
diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
index 17f01e5d6..1c8468e68 100644
--- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -104,14 +104,6 @@ Declare Reduction interp_red
     not contain evars.  Most tactics use [abstract] to reduce the load
     on [Defined] and to catch looping behavior early. *)
 
-(** The tactic [unify_abstract_renamify_rhs_reflexivity] calls
-    [renamify] on [RHS] and unifies that with [LHS]; and then costs
-    one [vm_compute] to prove the equality. *)
-Ltac unify_abstract_renamify_rhs_reflexivity :=
-  unify_transformed_rhs_abstract_tac
-    ltac:(renamify)
-           unify_tac
-           vm_cast_no_check.
 (** The tactic [unify_abstract_cbv_interp_rhs_reflexivity] runs the interpretation
     reduction strategies in [RHS] and unifies the result with [LHS],
     and does not use the vm (and hence does not fully reduce things,
@@ -204,7 +196,6 @@ Section with_round_up_list.
     {
       b : interp_flat_type Bounds.interp_base_type (codomain t);
       e' : Expr (pick_type input_bounds -> pick_type b);
-      e_final : Expr (pick_type input_bounds -> pick_type b);
       e_final_newtype : Expr (pick_type input_bounds -> pick_type given_output_bounds);
       e : Expr (domain t -> codomain t);
       e_pre_pkg : Expr (domain t -> codomain t);
@@ -230,8 +221,6 @@ Section with_round_up_list.
       (** ** post-wf-pipeline *)
       Hpost : e_pkg = PostWfBoundsPipeline _ opts e e_pre_pkg input_bounds;
       Hpost_correct : Some {| OutputType.input_expr := e ; OutputType.input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |} = e_pkg;
-      (** ** renaming *)
-      Hrenaming : e_final = e';
       (** ** bounds relaxation *)
       Hbounds_relax : Bounds.is_tighter_thanb b given_output_bounds = true;
       Hbounds_sane : pick_type given_output_bounds = pick_type b;
@@ -251,9 +240,9 @@ Section with_round_up_list.
       /\ cast_back_flat_const final_e_evar = fZ (cast_back_flat_const v').
   Proof using All.
     destruct side_conditions
-      as [He He_unnatize_for_wf Hwf Hpost_wf_pre_bounds Hpost Hpost_correct Hrenaming Hbounds_relax Hbounds_sane Hbounds_sane_refl Hevar Hv1 Hv2].
-    cbv [b e' e_final e_final_newtype e e_pre_pkg e_pkg] in *.
-    destruct evars as [b e' e_final e_final_newtype e e_pre_pkg e_pkg];
+      as [He He_unnatize_for_wf Hwf Hpost_wf_pre_bounds Hpost Hpost_correct Hbounds_relax Hbounds_sane Hbounds_sane_refl Hevar Hv1 Hv2].
+    cbv [b e' e_final_newtype e e_pre_pkg e_pkg] in *.
+    destruct evars as [b e' e_final_newtype e e_pre_pkg e_pkg];
       clear evars.
     destruct rexpr_sig as [? Hrexpr]; clear rexpr_sig.
     assert (Hwf' : Wf e)
@@ -291,7 +280,7 @@ Ltac refine_PipelineSideConditions_constructor :=
   lazymatch goal with
   | [ |- PipelineSideConditions ?opts ?evars _ ]
     => simple refine {| Hevar := _ |};
-       cbv [b e' e_final e_final_newtype e e_pre_pkg e_pkg proj1_sig]
+       cbv [b e' e_final_newtype e e_pre_pkg e_pkg proj1_sig]
   end.
 Ltac refine_with_pipeline_correct opts :=
   lazymatch goal with
@@ -341,8 +330,6 @@ Ltac solve_post_reified_side_conditions :=
    unify_abstract_vm_compute_rhs_reflexivity |
    (** ** post-wf pipeline gives [Some _] *)
    unify_abstract_rhs_reflexivity |
-   (** ** renaming binders *)
-   unify_abstract_renamify_rhs_reflexivity |
    (** ** computed output bounds are not looser than the given output bounds *)
    (** we do subst and we don't [vm_compute] first because we want to
        get an error message that displays the bounds *)