The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hi, Jason --

Thomas Braibant wrote some nice tactics that can perform timing. The github repository is located here:

https://github.com/braibant/Timing-plugin

I've used it and it works quite well.

On Wed, Jan 2, 2013 at 5:15 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Hi,

Is there a way to profile Ltac code, i.e., to get a list of how much time is spent in each Ltac fragment (such as [apply MyTheorem], [apply f_equal], [myTac a b c])?

Thanks.

-Jason

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/