diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-14 01:19:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-14 01:19:02 +0200 |
| commit | 2b03bdd3e19016fb107446713f9a8e786bea00e2 (patch) | |
| tree | 21e7819caa2e500320d412021fb82e2c1a382ffe /pretyping | |
| parent | 9f8cea70ed5c6bff03eada4f2808be0da7fa4412 (diff) | |
| parent | 22a8bf74be802a591e2e691ed5fb457e9b71ca21 (diff) | |
Merge PR #7771: Tweak printing boxes for unicode binders
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions