| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
It seems we have no grammar rule that parses floats, so I'm
parsing an integer, but the whole machinery supports floats.
|
|
Changes:
- data structures are purely functional (so retracting do work)
- profiling data flows towards master using the feedback bus
- master aggregates the data on printing
|
|
using a custom feedback message in response to "Show Ltac Profile."
|
|
|
|
|
|
|
