diff options
| author | Jason Gross | 2016-05-14 23:09:20 -0400 |
|---|---|---|
| committer | Jason Gross | 2016-06-05 22:09:40 -0400 |
| commit | 13e11b6aec1444071dc3787da15e89a6bc0eb0dc (patch) | |
| tree | c1e80a141882c806d40a0159be9dbca4be0aa848 /ltac | |
| parent | 739ead8b2d70f978e31f793234d7a633636742a1 (diff) | |
Synchronize the profiler state with the document
This is suboptimal, because mutation leaves room for subtle bugs, but
rewriting @tebbi's code to be functional was a pain, and not something I
could figure out how to do easily. I'm working under the assumption
that there is no sharing in a single treenode, which I'm not completely
sure is valid. That said, a few simple tests seem to indicate that this
works as expected.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/profile_ltac_tactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index 0c4e0b0757..ce00c29202 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -19,7 +19,7 @@ END;; VERNAC COMMAND EXTEND StartProfiling CLASSIFIED AS SIDEFF - [ "Start" "Profiling" ] -> [ reset_profile(); set_profiling true ] + [ "Start" "Profiling" ] -> [ set_profiling true ] END VERNAC COMMAND EXTEND StopProfiling CLASSIFIED AS SIDEFF |