diff options
| author | Gaëtan Gilbert | 2021-01-11 12:09:19 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-01-11 12:09:19 +0100 |
| commit | 27a9a28e8628c94910a08efc2f611e91e3e553bb (patch) | |
| tree | 67b140d9f47a7e50a63e8da79c17662209b41c8e /vernac | |
| parent | ffb482f0c18bff2c65dcc9cd2b65bd20b398245d (diff) | |
Respect print_universes in detype_instance
This partially fixes #13732 and matches what we do in detype_sort
Diffstat (limited to 'vernac')
0 files changed, 0 insertions, 0 deletions