aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-09-05 17:34:25 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-09-05 17:34:25 -0400
commitb87cd7cb1d6f704807f12e0a259b910e6b7ee2c0 (patch)
treee3c8cf012eb893d8872c3a4e7008dd2248b58432 /src
parentd664d0b423a01b336ec0f26c8f786b8d3a178dbe (diff)
Fix more commented out alternatives
Diffstat (limited to 'src')
-rw-r--r--src/Specific/IntegrationTestLadderstep130.v3
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). }