diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-18 18:17:52 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-18 18:17:52 -0400 |
| commit | fe02e394fa240cf52c103a17be3686a2d3b49560 (patch) | |
| tree | 512b0e668802491fd431dbe958738ebdde366874 | |
| parent | c5312bea6a6cc9dafe7ec20adaa5897546f48c20 (diff) | |
Add convenience for supporting uint8
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v index ee6929020..5ae472e62 100644 --- a/src/Compilers/Z/Bounds/Pipeline.v +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -29,12 +29,18 @@ Ltac refine_reflectively32_with opts := refine_reflectively_gen [32; 64] opts. Ltac refine_reflectively128_with_bool_with opts := refine_reflectively_gen [1; 128; 256] opts. Ltac refine_reflectively64_with_bool_with opts := refine_reflectively_gen [1; 64; 128] opts. Ltac refine_reflectively32_with_bool_with opts := refine_reflectively_gen [1; 32; 64] opts. +Ltac refine_reflectively128_with_uint8_with opts := refine_reflectively_gen [8; 128; 256] opts. +Ltac refine_reflectively64_with_uint8_with opts := refine_reflectively_gen [8; 64; 128] opts. +Ltac refine_reflectively32_with_uint8_with opts := refine_reflectively_gen [8; 32; 64] 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. Ltac refine_reflectively128_with_bool := refine_reflectively128_with_bool_with default_PipelineOptions. Ltac refine_reflectively64_with_bool := refine_reflectively64_with_bool_with default_PipelineOptions. Ltac refine_reflectively32_with_bool := refine_reflectively32_with_bool_with default_PipelineOptions. +Ltac refine_reflectively128_with_uint8 := refine_reflectively128_with_uint8_with default_PipelineOptions. +Ltac refine_reflectively64_with_uint8 := refine_reflectively64_with_uint8_with default_PipelineOptions. +Ltac refine_reflectively32_with_uint8 := refine_reflectively32_with_uint8_with default_PipelineOptions. (** Convenience notations for options *) Definition anf := {| Pipeline.Definition.anf := true |}. @@ -42,5 +48,6 @@ Definition default := default_PipelineOptions. (** The default *) Ltac refine_reflectively_with_bool_with opts := refine_reflectively64_with_bool_with opts. +Ltac refine_reflectively_with_uint8_with opts := refine_reflectively64_with_uint8_with opts. Ltac refine_reflectively_with opts := refine_reflectively64_with opts. Ltac refine_reflectively := refine_reflectively_with default. |