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.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 5eac3e2b9c..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
@@ -161,6 +159,7 @@ val ppobj : Libobject.obj -> unit
val cast_kind_display : Constr.cast_kind -> string
val constr_display : Constr.constr -> unit
val print_pure_constr : Constr.types -> unit
+val print_pure_econstr : EConstr.types -> unit
val pploc : Loc.t -> unit