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 /dev/include | |
| 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 'dev/include')
| -rw-r--r-- | dev/include | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/include b/dev/include index 58fff078be..a8c4e1d493 100644 --- a/dev/include +++ b/dev/include @@ -38,6 +38,7 @@ #install_printer (* universes *) ppuniverses;; #install_printer (* univ level *) ppuni_level;; #install_printer (* univ context *) ppuniverse_context;; +#install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; |