aboutsummaryrefslogtreecommitdiff
path: root/API/API.mllib
diff options
context:
space:
mode:
authorJason Gross2017-12-11 02:23:10 -0500
committerJason Gross2017-12-14 12:05:50 -0500
commit40aca595dd8e26373bfa4f6b6d4cd7d43a933210 (patch)
tree3fef33ca12ba2bab8ce0efacf6cec6f640b3497c /API/API.mllib
parentb270ad686075e5579dc3826fafdc324ea339785c (diff)
Add tactics to reset and display the Ltac profile
This is useful for tactics that run a bunch of tests and need to display the profile for each of them.
Diffstat (limited to 'API/API.mllib')
0 files changed, 0 insertions, 0 deletions