diff options
| author | Jason Gross | 2016-05-15 16:05:11 -0400 |
|---|---|---|
| committer | Jason Gross | 2016-06-05 22:09:41 -0400 |
| commit | 9b0376731de3b71a7461747d12763becca1e5399 (patch) | |
| tree | 4eeaff5d0238034a7232e8b5778419dcd85444aa /plugins/syntax/string_syntax.ml | |
| parent | 13e11b6aec1444071dc3787da15e89a6bc0eb0dc (diff) | |
Make Ltac Profiling an setting
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions