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.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dev/top_printers.ml') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b18cbbd7b..cb1abc4a9 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -209,11 +209,11 @@ let ppuniverse_instance l = pp (Instance.pr prlev l) let ppuniverse_context l = pp (pr_universe_context prlev l) let ppuniverse_context_set l = pp (pr_universe_context_set prlev l) let ppuniverse_subst l = pp (Univ.pr_universe_subst l) -let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l) +let ppuniverse_opt_subst l = pp (UnivSubst.pr_universe_opt_subst l) let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l) let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l) let ppconstraints c = pp (pr_constraints Level.pr c) -let ppuniverseconstraints c = pp (Universes.Constraints.pr c) +let ppuniverseconstraints c = pp (UnivProblem.Set.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -- cgit v1.2.3