aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.mli
diff options
context:
space:
mode:
Diffstat (limited to 'dev/top_printers.mli')
-rw-r--r--dev/top_printers.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 4d874cdd12..cb32d2294c 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -145,8 +145,6 @@ val ppevar_universe_context : UState.t -> unit
val ppconstraints : Univ.Constraint.t -> unit
val ppuniverseconstraints : UnivProblem.Set.t -> unit
val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
-val ppcumulativity_info : Univ.CumulativityInfo.t -> unit
-val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit
val ppuniverses : UGraph.t -> unit
val ppnamedcontextval : Environ.named_context_val -> unit