diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-22 01:22:21 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:07 +0100 |
commit | 5b2f29e461d7dfb1336117050cc8c5d510025bf1 (patch) | |
tree | 4df78094c9503552f60bcda725f600bacc8ed36c /vernac/metasyntax.ml | |
parent | 87a8d6c24fa5d014380340fc09647bcd53b9fb5e (diff) |
More structured printing in unicode notations for binders.
Diffstat (limited to 'vernac/metasyntax.ml')
0 files changed, 0 insertions, 0 deletions