| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
| |
I'm not sure if they belong in profile_ltac, or in extratactics, or,
perhaps, in a separate plugin. But I'd find it very useful to have a
version of `time` that works on constr evaluation, which is what this
commit provides.
I'm not sure that I've picked good naming conventions for the tactics,
either.
|
|
|
|
|
| |
This is useful for tactics that run a bunch of tests and need to display
the profile for each of them.
|
|
|
|
|
|
| |
This fixes #6378. Previously the ML module was never declared anywhere.
Thanks to @cmangin for the pointer.
|
| |
|
| |
|
| |
|
|
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|