diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-17 01:38:06 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-17 01:38:06 -0400 |
| commit | 7884130a89d07f4bbe1465126c06ca4c3927cb81 (patch) | |
| tree | b033b2b3c4808e57b9a92f53f010dc16fff5ebe9 /src | |
| parent | ffe32c0bbd6c940db25c7c643e7e566f5f9745db (diff) | |
Ltac scope interprets some notations as errors, so we make anf a definition
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v index 8108e4389..9259aedd8 100644 --- a/src/Compilers/Z/Bounds/Pipeline.v +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -27,7 +27,7 @@ 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 |}. +Definition anf := {| Pipeline.Definition.anf := true |}. (** The default *) Ltac refine_reflectively_with opts := refine_reflectively64_with opts. |