diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-17 12:29:41 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-17 12:29:41 -0400 |
| commit | cf1cbc66173e78a489cfc38161270544a418301b (patch) | |
| tree | 32b89ac0d962341c9a0032609466afd16b435b50 /src/Compilers/Z/Bounds | |
| parent | 98a525f328cf2c7c5c9794a171974f03174a9523 (diff) | |
Add bool into P256
Diffstat (limited to 'src/Compilers/Z/Bounds')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v index c2ce603f5..ee6929020 100644 --- a/src/Compilers/Z/Bounds/Pipeline.v +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -38,8 +38,9 @@ Ltac refine_reflectively32_with_bool := refine_reflectively32_with_bool_with def (** Convenience notations for options *) Definition anf := {| Pipeline.Definition.anf := true |}. +Definition default := default_PipelineOptions. (** The default *) Ltac refine_reflectively_with_bool_with opts := refine_reflectively64_with_bool_with opts. Ltac refine_reflectively_with opts := refine_reflectively64_with opts. -Ltac refine_reflectively := refine_reflectively_with default_PipelineOptions. +Ltac refine_reflectively := refine_reflectively_with default. |