diff options
| author | Pierre-Marie Pédrot | 2018-09-13 13:47:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-21 13:09:21 +0200 |
| commit | aaee23f06e4ac345238cb84edc1c16fafe6b6b3d (patch) | |
| tree | b42f3df8504a5c258f4b5c213d1b3d47158a4a67 /dev | |
| parent | 51dad02266f0bea735d496839c559b472bc4553e (diff) | |
Store universe binder names as a mere list of names.
This is the only information we care about. The printing mechanism is only
called on polymorphic constants, as the naming of global monomorphic levels
is performed in another module.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions