diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-17 12:23:44 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-17 12:25:31 -0400 |
| commit | 90ab3b5a3941ebb1a83dcc06b6a62be3c3e24e6f (patch) | |
| tree | a3fff4516411cda8f14d2d983b828ee93648ba9c /src/Specific/IntegrationTestMontgomeryP256.v | |
| parent | 17b018fe9d134028da41f397c41d1f4149dfe742 (diff) | |
Finish MontgomeryP256 (less conditional subtract)
Diffstat (limited to 'src/Specific/IntegrationTestMontgomeryP256.v')
| -rw-r--r-- | src/Specific/IntegrationTestMontgomeryP256.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/Specific/IntegrationTestMontgomeryP256.v b/src/Specific/IntegrationTestMontgomeryP256.v index 631ea3209..1bb8fc23d 100644 --- a/src/Specific/IntegrationTestMontgomeryP256.v +++ b/src/Specific/IntegrationTestMontgomeryP256.v @@ -63,9 +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.*) - Ltac reify_debug_level ::= constr:(3%nat). - Typeclasses eauto := debug. - Time admit; refine_reflectively. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *) + Time refine_reflectively. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) (*Show Ltac Profile.*) (* total time: 19.632s @@ -109,6 +107,6 @@ Section BoundedField25p5. │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s *) - Time Admitted. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *) + Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *) -End BoundedField25p5. +Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *) |