diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-23 09:59:30 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-23 09:59:30 +0100 |
| commit | 89d14fa4f16e9741108887177d43d34675261d22 (patch) | |
| tree | b2d97d58db1a1220d42639ccbd5649b1036762a7 /vernac/mltop.mli | |
| parent | a4e4bf422093612c87bf6a55b98b8b7a7317c18a (diff) | |
| parent | e19d39cc2796345d531b5a2d7dd33980f8989bfb (diff) | |
Merge PR #6628: [printing] Remove duplicate definitions of pr_lident and pr_lname
Diffstat (limited to 'vernac/mltop.mli')
0 files changed, 0 insertions, 0 deletions