aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/profile_ltac.mli
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Merge PR #6381: A version of [time] that works on constr evaluationGravatar Maxime Dénès2017-12-18
|\
| * Add named timers to LtacProfGravatar Jason Gross2017-12-14
* | Fix #5081 by more fine-grained LtacProf recordingGravatar Jason Gross2017-12-12
|/
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17