aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6ae5125f6d..1be72759c9 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -8,7 +8,6 @@
(* Printers for the ocaml toplevel. *)
-open API
open Util
open Pp
open Names
@@ -215,6 +214,8 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
let ppuniverse_context_future c =
let ctx = Future.force c in
ppuniverse_context ctx
+let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
+let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c)
let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
let ppnamedcontextval e =
pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))