diff options
| author | Hugo Herbelin | 2016-11-20 17:58:07 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-12-02 15:21:37 +0100 |
| commit | 4e551415f20ad696c319b32b349e4499c2505388 (patch) | |
| tree | 77263535913a744b141a1644cfbfbf55a2c33130 /kernel/type_errors.mli | |
| parent | 17c3f8e2d339e5b6f60c89ad17e578d786d2b9ca (diff) | |
Protect printing of ltac's "context [...]" from possible collision
with user-level notations by inserting spaces.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions