diff options
| author | Matthieu Sozeau | 2014-03-12 12:21:40 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:57 +0200 |
| commit | ca318cd0d21ce157a3042b600ded99df6face25e (patch) | |
| tree | ca60f1337c739f46053aa904a1212c209052ef2e /kernel/mod_typing.ml | |
| parent | df5e18302e113370906d9ca0b2a2e96dcaccbf0a (diff) | |
Fix issue #88: restrict_universe_context was wrongly forgetting about constraints,
and keeping spurious equalities. simplify_universe_context is correct, although
it might keep unused universes around (it's the responsibility of the tactics to
not produce unused universes then).
Add printer for future universe contexts for debugging.
Diffstat (limited to 'kernel/mod_typing.ml')
0 files changed, 0 insertions, 0 deletions