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 | |
| 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')
| -rw-r--r-- | dev/include | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 3 |
2 files changed, 4 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;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 857a989dc7..ec7716356c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -192,6 +192,9 @@ let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l) let ppconstraints_map c = pp (Universes.pr_constraints_map c) let ppconstraints c = pp (pr_constraints c) let ppuniverseconstraints c = pp (UniverseConstraints.pr c) +let ppuniverse_context_future c = + let ctx = Future.force c in + ppuniverse_context ctx let ppenv e = pp (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++ |