diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:22:59 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:22:59 +0100 |
commit | a40fb961c8ffeeb03769404cacda8bd6cff17417 (patch) | |
tree | 7105d621bc16f825c1f309e3d5b7720b1b1513ec /vernac/classes.mli | |
parent | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (diff) | |
parent | 66973ce17e32a3c692a5b0032f38300ec8cc36d3 (diff) |
Merge PR #6893: Cleanup UState API usage
Diffstat (limited to 'vernac/classes.mli')
0 files changed, 0 insertions, 0 deletions