diff options
| author | Arnaud Spiwack | 2014-09-30 11:17:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-02 11:17:51 +0200 |
| commit | 0e5c76991d9159bc182baf65d7d44f135c8dfeea (patch) | |
| tree | 8ac37c1d24d16e7c1c12f574daef14cbb5910b1e /lib | |
| parent | 68846802a7be637ec805a5e374655a426b5723a5 (diff) | |
Print type and environment of unsolved holes.
Was just printed in the case of internal holes.
Also: replace [str] by [strbrk] in error message of unsolved holes for better layout.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions