aboutsummaryrefslogtreecommitdiff
path: root/ltac/profile_ltac.ml
AgeCommit message (Expand)Author
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