diff options
Diffstat (limited to 'src/Compilers/Z/Bounds/Pipeline.v')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v index 0db061ec4..4e3696854 100644 --- a/src/Compilers/Z/Bounds/Pipeline.v +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -15,13 +15,17 @@ Module Export Exports. Export ReflectiveTactics.Exports. End Exports. -Ltac refine_reflectively_gen allowable_bit_widths := +Ltac refine_reflectively_gen allowable_bit_widths opts := refine_to_reflective_glue allowable_bit_widths; - do_reflective_pipeline. + do_reflective_pipeline opts. -Ltac refine_reflectively128 := refine_reflectively_gen (128::256::nil)%nat%list. -Ltac refine_reflectively64 := refine_reflectively_gen (64::128::nil)%nat%list. -Ltac refine_reflectively32 := refine_reflectively_gen (32::64::nil)%nat%list. +Ltac refine_reflectively128_with opts := refine_reflectively_gen (128::256::nil)%nat%list opts. +Ltac refine_reflectively64_with opts := refine_reflectively_gen (64::128::nil)%nat%list opts. +Ltac refine_reflectively32_with opts := refine_reflectively_gen (32::64::nil)%nat%list opts. +Ltac refine_reflectively128 := refine_reflectively128_with default_PipelineOptions. +Ltac refine_reflectively64 := refine_reflectively64_with default_PipelineOptions. +Ltac refine_reflectively32 := refine_reflectively32_with default_PipelineOptions. (** The default *) -Ltac refine_reflectively := refine_reflectively64. +Ltac refine_reflectively_with opts := refine_reflectively64_with opts. +Ltac refine_reflectively := refine_reflectively_with default_PipelineOptions. |