diff options
Diffstat (limited to 'src/Compilers/Z/Bounds/Pipeline.v')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v index 4e3696854..8108e4389 100644 --- a/src/Compilers/Z/Bounds/Pipeline.v +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -26,6 +26,9 @@ Ltac refine_reflectively128 := refine_reflectively128_with default_PipelineOptio Ltac refine_reflectively64 := refine_reflectively64_with default_PipelineOptions. Ltac refine_reflectively32 := refine_reflectively32_with default_PipelineOptions. +(** Convenience notations for options *) +Notation anf := {| Pipeline.Definition.anf := true |}. + (** The default *) Ltac refine_reflectively_with opts := refine_reflectively64_with opts. Ltac refine_reflectively := refine_reflectively_with default_PipelineOptions. |