diff options
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() ++ |