diff options
| -rw-r--r-- | src/Specific/IntegrationTestLadderstep130.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v index 4dd01d018..e97784c5a 100644 --- a/src/Specific/IntegrationTestLadderstep130.v +++ b/src/Specific/IntegrationTestLadderstep130.v @@ -109,12 +109,13 @@ Section BoundedField25p5. Set Ltac Profiling. (* Time Glue.refine_to_reflective_glue (128::256::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). } |