From 302adae094bbf76d8c951c557c85acb12a97aedc Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 21:27:15 +0200 Subject: Split off Universes functions about substitutions and constraints --- dev/top_printers.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dev/top_printers.mli') diff --git a/dev/top_printers.mli b/dev/top_printers.mli index c23ba964c..63d7d5805 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -139,11 +139,11 @@ val ppuniverse_instance : Univ.Instance.t -> unit val ppuniverse_context : Univ.UContext.t -> unit val ppuniverse_context_set : Univ.ContextSet.t -> unit val ppuniverse_subst : Univ.universe_subst -> unit -val ppuniverse_opt_subst : Universes.universe_opt_subst -> unit +val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit val ppuniverse_level_subst : Univ.universe_level_subst -> unit val ppevar_universe_context : UState.t -> unit val ppconstraints : Univ.Constraint.t -> unit -val ppuniverseconstraints : Universes.Constraints.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 -- cgit v1.2.3