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 | |
| parent | 98a525f328cf2c7c5c9794a171974f03174a9523 (diff) | |
Add bool into P256
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 3 | ||||
| -rw-r--r-- | src/Specific/IntegrationTestMontgomeryP256.v | 2 |
2 files changed, 3 insertions, 2 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. diff --git a/src/Specific/IntegrationTestMontgomeryP256.v b/src/Specific/IntegrationTestMontgomeryP256.v index 1bb8fc23d..589cd616a 100644 --- a/src/Specific/IntegrationTestMontgomeryP256.v +++ b/src/Specific/IntegrationTestMontgomeryP256.v @@ -63,7 +63,7 @@ Section BoundedField25p5. (*apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).*) (* jgross start here! *) (*Set Ltac Profiling.*) - Time refine_reflectively. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) + Time refine_reflectively_with_bool_with default. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) (*Show Ltac Profile.*) (* total time: 19.632s |