aboutsummaryrefslogtreecommitdiff
path: root/ltac/profile_ltac.ml
AgeCommit message (Expand)Author
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2016-09-29LtacProf cutoff is for total percent, not timeJason Gross
2016-09-29-profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)Enrico Tassi
2016-09-27LtacProf: "Show Ltac Profile CutOff $N" (fix #5080)Enrico Tassi
2016-09-13LtacProp: fix reset_profile (fix #5079)Enrico Tassi
2016-09-11Fix newlines in printout of LtacProfJason Gross
2016-09-11Revert the LtacProf tactic table headerJason Gross
2016-09-07ltacprof: rec-calls are coaleshedEnrico Tassi
2016-09-05profile_ltac: rewritten to be purely functional and STM awareEnrico Tassi
2016-08-23Fix bug #4914: LtacProf printout has too many newlines.Pierre-Marie Pédrot
2016-08-18Fix bug #4939: LtacProf prints tactic notations weirdly.Pierre-Marie Pédrot
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-20LtacProf reports structured results (pr/209)CJ Bell
2016-06-16Fix another missing newlineJason Gross
2016-06-16Fix a printing typoJason Gross
2016-06-14Commenting out debugging code.Pierre-Marie Pédrot
2016-06-14Correct use of printing primitives.Pierre-Marie Pédrot
2016-06-14Better coding style (semantics).Pierre-Marie Pédrot
2016-06-14Better coding style (syntax).Pierre-Marie Pédrot
2016-06-14Adding Coq headers.Pierre-Marie Pédrot
2016-06-14Moving back Ltac profiling to the Ltac folder.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 18:27:27 +0000