diff options
| author | Pierre-Marie Pédrot | 2018-09-11 11:00:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-21 13:09:21 +0200 |
| commit | 51dad02266f0bea735d496839c559b472bc4553e (patch) | |
| tree | a6a18abe9b8d1ee74c848f6dcd302c08adb89da6 /kernel/type_errors.ml | |
| parent | 4c28e0597067d81f5ee7e8b2b2e668f4d45e973f (diff) | |
Removing calls to AUContext.instance.
We simply declare the bound universes with their user-facing name in the
evarmap and call all printing functions on uninstantiated terms. We had to
tweak the universe name declaring function so that it would work properly
with bound universe variables and handle sections correctly.
This changes the output of polymorphic definitions with unnamed universe
variables. Now they are printed as Var(i) instead of the Module.n uid
that came from their absolute name.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions