diff options
-rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 3 | ||||
-rw-r--r-- | src/Specific/IntegrationTestMontgomeryP256.v | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v index c2ce603f5..ee6929020 100644 --- a/src/Compilers/Z/Bounds/Pipeline.v +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -38,8 +38,9 @@ Ltac refine_reflectively32_with_bool := refine_reflectively32_with_bool_with def (** Convenience notations for options *) Definition anf := {| Pipeline.Definition.anf := true |}. +Definition default := default_PipelineOptions. (** The default *) Ltac refine_reflectively_with_bool_with opts := refine_reflectively64_with_bool_with opts. Ltac refine_reflectively_with opts := refine_reflectively64_with opts. -Ltac refine_reflectively := refine_reflectively_with default_PipelineOptions. +Ltac refine_reflectively := refine_reflectively_with default. diff --git a/src/Specific/IntegrationTestMontgomeryP256.v b/src/Specific/IntegrationTestMontgomeryP256.v index 1bb8fc23d..589cd616a 100644 --- a/src/Specific/IntegrationTestMontgomeryP256.v +++ b/src/Specific/IntegrationTestMontgomeryP256.v @@ -63,7 +63,7 @@ Section BoundedField25p5. (*apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).*) (* jgross start here! *) (*Set Ltac Profiling.*) - Time refine_reflectively. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) + Time refine_reflectively_with_bool_with default. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) (*Show Ltac Profile.*) (* total time: 19.632s |