summaryrefslogtreecommitdiff
path: root/dev/top_printers.mli
diff options
context:
space:
mode:
Diffstat (limited to 'dev/top_printers.mli')
-rw-r--r--dev/top_printers.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index dad6dcc1..63d7d580 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -87,7 +87,7 @@ val ppclosedglobconstr : Ltac_pretype.closed_glob_constr -> unit
val ppclosedglobconstridmap :
Ltac_pretype.closed_glob_constr Names.Id.Map.t -> unit
-val ppglobal : Globnames.global_reference -> unit
+val ppglobal : Names.GlobRef.t -> unit
val ppconst :
Names.KerName.t * (Constr.constr, 'a) Environ.punsafe_judgment -> unit
@@ -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