aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/ltacprof.v
AgeCommit message (Collapse)Author
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
Fixes #12196
2016-06-05Improve a comment in the test suiteJason Gross
2016-06-05Make Ltac Profiling an settingJason Gross
2016-06-05LtacProf for Coq trunkJason Gross
This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk.