diff options
| author | Pierre-Marie Pédrot | 2018-09-13 15:14:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-21 13:09:21 +0200 |
| commit | 138f7c628e546775b381fa1f8805acc433839684 (patch) | |
| tree | 7c3812765e5d28a4574ad220c3cc87824546e7c5 /dev | |
| parent | aaee23f06e4ac345238cb84edc1c16fafe6b6b3d (diff) | |
Best-effort hack to provide a meaningful name for anonymous bound universes.
This restores the old behaviour that was printing qualified global names as
a representation of anonymous bound universes, at the cost of a ugly hack.
Ideally this should be handled by the callers, but for the time being the
trade-off is probably OK.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions