aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tactic_debug.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-11-21 13:24:57 +0100
committerMaxime Dénès2017-11-21 13:24:57 +0100
commit74e60947d78e3610312aa1702f12143841c5a7cf (patch)
treecdb498ff262f98d188a86af1fb8547c318db2557 /plugins/ltac/tactic_debug.ml
parent33c5603dfe76cbd96944fd38d5fa6699c32a9355 (diff)
parent8794dbd18c61109298b827146bcd2b370f5798bd (diff)
Merge PR #6178: Have the coq_makefile timing test-suite print more
Diffstat (limited to 'plugins/ltac/tactic_debug.ml')
0 files changed, 0 insertions, 0 deletions