diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-18 00:41:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-25 17:17:44 +0200 |
| commit | c9f9a159818c138af3b8d8a3a1023a66b88be207 (patch) | |
| tree | 08f3a8ecb129753981150169e50cf5dd498623d0 /tools/fake_ide.ml | |
| parent | 9bff82239c2a6412a26ae3c5faab42a9c9d2ccb1 (diff) | |
[feedback] Add optional ?loc parameter to loggers.
This is a first step to relay location info in an uniform way, as needed
by warnings and other mechanisms.
The location info remains unused for now, but coqtop printing could take
advantage of it if so wished.
Diffstat (limited to 'tools/fake_ide.ml')
0 files changed, 0 insertions, 0 deletions