Fix commented out alternate version in ladderstep

1 files changed, 2 insertions, 1 deletions

diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v
index ad0037245..adafa6d56 100644
--- a/src/Specific/X25519/C64/ladderstep.v
+++ b/src/Specific/X25519/C64/ladderstep.v
@@ -144,12 +144,13 @@ Section BoundedField25p5.
     Set Ltac Profiling.
     (*
     Time Glue.refine_to_reflective_glue (64::128::nil)%nat%list.
-    Time ReflectiveTactics.refine_with_pipeline_correct.
+    Time ReflectiveTactics.refine_with_pipeline_correct default.
     { Time ReflectiveTactics.do_reify. }
     { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
     { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
     { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
     { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
     { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. }
     { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. }
     { Time SubstLet.subst_let; clear; abstract vm_cast_no_check (eq_refl true). }