diff options
| author | Hugo Herbelin | 2017-11-07 14:21:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-07 14:21:06 +0100 |
| commit | 4e23d4b7ba4910e7c41d2cbc4c3bff12ba153558 (patch) | |
| tree | 21b280a495a118cce794c40a37db65b99abb6a90 /API/API.mli | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
Hack to restore printing of glob_constr in debugger.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions