diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-17 17:34:22 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-17 17:34:22 -0400 |
| commit | b8b2bf3c9532d5ed1a27c7773b728781456145b4 (patch) | |
| tree | 5543679039532f4785697d1e0b3dd985ac81a8d2 /src/Specific/IntegrationTestMontgomeryP256.v | |
| parent | cf59ecb04ca39e4f878d10fdffd92474e8421af0 (diff) | |
Enable profiling in integration test mont 256
Diffstat (limited to 'src/Specific/IntegrationTestMontgomeryP256.v')
| -rw-r--r-- | src/Specific/IntegrationTestMontgomeryP256.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/IntegrationTestMontgomeryP256.v b/src/Specific/IntegrationTestMontgomeryP256.v index 589cd616a..90aae7723 100644 --- a/src/Specific/IntegrationTestMontgomeryP256.v +++ b/src/Specific/IntegrationTestMontgomeryP256.v @@ -62,9 +62,9 @@ Section BoundedField25p5. sig_dlet_in_rhs_to_context. (*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.*) + Set Ltac Profiling. Time refine_reflectively_with_bool_with default. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - (*Show Ltac Profile.*) + Show Ltac Profile. (* total time: 19.632s tactic local total calls max |