diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-17 01:28:36 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-17 01:28:36 -0400 |
| commit | ffe32c0bbd6c940db25c7c643e7e566f5f9745db (patch) | |
| tree | 7e53cadadf7d1aadbe25e5116fbc72896eb3da68 /src | |
| parent | 57ddc251461ed5806e6f2fd2c98a6555f18f58fe (diff) | |
Fix a typo in prev commit, add convenience notation
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 3 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Definition.v | 2 |
2 files changed, 4 insertions, 1 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. diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v index 675c4d2d0..e7c267d65 100644 --- a/src/Compilers/Z/Bounds/Pipeline/Definition.v +++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v @@ -89,7 +89,7 @@ Definition PostWfPipeline let e := SimplifyArith e in let e := InlineConst e in let e := SimplifyArith e in - let e := if opts.(anormal) then ANormal e else e in + let e := if opts.(anf) then ANormal e else e in let e := InlineConst e in (*let e := CSE false e in*) let e := MapCast _ e input_bounds in |