diff options
| author | Gabriel Kerneis | 2014-05-15 12:30:03 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-05-15 12:30:03 +0100 |
| commit | f12a48f09bc6bc44c8cac0de6f4ebb8ab2a14cb6 (patch) | |
| tree | 20a0a437f9b965bddc136e9d31c86e30e035cd4c /src/pretty_print.ml | |
| parent | fa39ead01f773e1967414ce421fdd86d476a96fe (diff) | |
Check name_sect during parsing
Diffstat (limited to 'src/pretty_print.ml')
0 files changed, 0 insertions, 0 deletions