diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-15 18:09:44 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-05-17 17:16:47 -0400 |
| commit | 2674181a88e4eea11e11fca676c257886b3805dd (patch) | |
| tree | 2f9cb42827b08e4e704ea1d4312d0577ff9580af /src | |
| parent | 002b62a5575318d20bea702bed7a38d39cfce8a1 (diff) | |
Allow 'bool' in output
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v index 9259aedd8..fd61fefb4 100644 --- a/src/Compilers/Z/Bounds/Pipeline.v +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -19,9 +19,9 @@ Ltac refine_reflectively_gen allowable_bit_widths opts := refine_to_reflective_glue allowable_bit_widths; do_reflective_pipeline opts. -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_with opts := refine_reflectively_gen (1::128::256::nil)%nat%list opts. +Ltac refine_reflectively64_with opts := refine_reflectively_gen (1::64::128::nil)%nat%list opts. +Ltac refine_reflectively32_with opts := refine_reflectively_gen (1::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. |