deprecate Pp.std_ppcmds type alias

7 files changed, 44 insertions, 44 deletions

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 8f38e9d34..718917ab3 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -34,7 +34,7 @@ type structured_constant =
   | Const_univ_level of Univ.universe_level
   | Const_type of Univ.universe
 
-val pp_struct_const : structured_constant -> Pp.std_ppcmds
+val pp_struct_const : structured_constant -> Pp.t
 
 type reloc_table = (tag * int) array
 
@@ -163,8 +163,8 @@ type comp_env = {
     in_env : vm_env ref          (** the variables that are accessed        *)
   }
 
-val pp_bytecodes : bytecodes -> Pp.std_ppcmds
-val pp_fv_elem : fv_elem -> Pp.std_ppcmds
+val pp_bytecodes : bytecodes -> Pp.t
+val pp_fv_elem : fv_elem -> Pp.t
 
 (*spiwack: moved this here because I needed it for retroknowledge *)
 type block =
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 3cd02fb9f..f1d0e4279 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -107,9 +107,9 @@ val subst_substituted : substitution -> 'a substituted -> 'a substituted
 (**/**)
 (* debugging *)
 val debug_string_of_subst : substitution -> string
-val debug_pr_subst : substitution -> Pp.std_ppcmds
+val debug_pr_subst : substitution -> Pp.t
 val debug_string_of_delta : delta_resolver -> string
-val debug_pr_delta : delta_resolver -> Pp.std_ppcmds
+val debug_pr_delta : delta_resolver -> Pp.t
 (**/**)
 
 (** [subst_mp sub mp] guarantees that whenever the result of the
diff --git a/kernel/names.mli b/kernel/names.mli
index 74d63c0ce..d111dd3c0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -57,7 +57,7 @@ sig
   val to_string : t -> string
   (** Converts a identifier into an string. *)
 
-  val print : t -> Pp.std_ppcmds
+  val print : t -> Pp.t
   (** Pretty-printer. *)
 
   module Set : Set.S with type elt = t
@@ -105,7 +105,7 @@ sig
   val hcons : t -> t
   (** Hashconsing over names. *)
 
-  val print : t -> Pp.std_ppcmds
+  val print : t -> Pp.t
   (** Pretty-printer (print "_" for [Anonymous]. *)
 
 end
@@ -187,7 +187,7 @@ sig
   val to_id : t -> Id.t
   (** Conversion to an identifier. *)
 
-  val print : t -> Pp.std_ppcmds
+  val print : t -> Pp.t
   (** Pretty-printer. *)
 
   module Set : Set.S with type elt = t
@@ -286,7 +286,7 @@ sig
   val debug_to_string : t -> string
   (** Same as [to_string], but outputs information related to debug. *)
 
-  val print : t -> Pp.std_ppcmds
+  val print : t -> Pp.t
 
   (** Comparisons *)
   val compare : t -> t -> int
@@ -365,9 +365,9 @@ sig
   (** Displaying *)
 
   val to_string : t -> string
-  val print : t -> Pp.std_ppcmds
+  val print : t -> Pp.t
   val debug_to_string : t -> string
-  val debug_print : t -> Pp.std_ppcmds
+  val debug_print : t -> Pp.t
 
 end
 
@@ -447,9 +447,9 @@ sig
   (** Displaying *)
 
   val to_string : t -> string
-  val print : t -> Pp.std_ppcmds
+  val print : t -> Pp.t
   val debug_to_string : t -> string
-  val debug_print : t -> Pp.std_ppcmds
+  val debug_print : t -> Pp.t
 
 end
 
@@ -609,7 +609,7 @@ val mk_label : string -> label
 val string_of_label : label -> string
 (** @deprecated Same as [Label.to_string]. *)
 
-val pr_label : label -> Pp.std_ppcmds
+val pr_label : label -> Pp.t
 (** @deprecated Same as [Label.print]. *)
 
 val label_of_id : Id.t -> label
@@ -695,7 +695,7 @@ val label : kernel_name -> Label.t
 val string_of_kn : kernel_name -> string
 (** @deprecated Same as [KerName.to_string]. *)
 
-val pr_kn : kernel_name -> Pp.std_ppcmds
+val pr_kn : kernel_name -> Pp.t
 (** @deprecated Same as [KerName.print]. *)
 
 val kn_ord : kernel_name -> kernel_name -> int
@@ -731,7 +731,7 @@ module Projection : sig
   val map : (constant -> constant) -> t -> t
 
   val to_string : t -> string
-  val print : t -> Pp.std_ppcmds
+  val print : t -> Pp.t
 
 end
 
@@ -776,10 +776,10 @@ val con_with_label : constant -> Label.t -> constant
 val string_of_con : constant -> string
 (** @deprecated Same as [Constant.to_string] *)
 
-val pr_con : constant -> Pp.std_ppcmds
+val pr_con : constant -> Pp.t
 (** @deprecated Same as [Constant.print] *)
 
-val debug_pr_con : constant -> Pp.std_ppcmds
+val debug_pr_con : constant -> Pp.t
 (** @deprecated Same as [Constant.debug_print] *)
 
 val debug_string_of_con : constant -> string
@@ -826,10 +826,10 @@ val mind_modpath : mutual_inductive -> ModPath.t
 val string_of_mind : mutual_inductive -> string
 (** @deprecated Same as [MutInd.to_string] *)
 
-val pr_mind : mutual_inductive -> Pp.std_ppcmds
+val pr_mind : mutual_inductive -> Pp.t
 (** @deprecated Same as [MutInd.print] *)
 
-val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds
+val debug_pr_mind : mutual_inductive -> Pp.t
 (** @deprecated Same as [MutInd.debug_print] *)
 
 val debug_string_of_mind : mutual_inductive -> string
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 4de373eb4..2fe555018 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -59,7 +59,7 @@ val check_subtype : AUContext.t check_function
 
 (** {6 Pretty-printing of universes. } *)
 
-val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds
+val pr_universes : (Level.t -> Pp.t) -> universes -> Pp.t
 
 (** {6 Dumping to a file } *)
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 02b02db89..d915fb8c9 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -892,7 +892,7 @@ module Instance : sig
 
     val subst_fn : universe_level_subst_fn -> t -> t
     
-    val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+    val pr : (Level.t -> Pp.t) -> t -> Pp.t
     val levels : t -> LSet.t
 end = 
 struct
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 99092a543..a4f2e26b6 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -37,7 +37,7 @@ sig
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
-  val pr : t -> Pp.std_ppcmds
+  val pr : t -> Pp.t
   (** Pretty-printing *)
 
   val to_string : t -> string
@@ -56,7 +56,7 @@ module LSet :
 sig 
   include CSig.SetS with type elt = universe_level
 	      
-  val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+  val pr : (Level.t -> Pp.t) -> t -> Pp.t
   (** Pretty-printing *)
 end
 
@@ -86,10 +86,10 @@ sig
   val make : Level.t -> t
   (** Create a universe representing the given level. *)
 
-  val pr : t -> Pp.std_ppcmds
+  val pr : t -> Pp.t
   (** Pretty-printing *)
 
-  val pr_with : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+  val pr_with : (Level.t -> Pp.t) -> t -> Pp.t
 
   val is_level : t -> bool
   (** Test if the universe is a level or an algebraic universe. *)
@@ -127,7 +127,7 @@ type universe = Universe.t
 
 (** Alias name. *)
 
-val pr_uni : universe -> Pp.std_ppcmds
+val pr_uni : universe -> Pp.t
 	      
 (** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... 
    Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
@@ -218,7 +218,7 @@ sig
   (** [subst_union x y] favors the bindings of the first map that are [Some],
       otherwise takes y's bindings. *)
 
-  val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+  val pr : ('a -> Pp.t) -> 'a t -> Pp.t
   (** Pretty-printing *)
 end
 
@@ -270,7 +270,7 @@ sig
   val subst_fn : universe_level_subst_fn -> t -> t
   (** Substitution by a level-to-level function. *)
 
-  val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds
+  val pr : (Level.t -> Pp.t) -> t -> Pp.t
   (** Pretty-printing, no comments *)
 
   val levels : t -> LSet.t
@@ -463,18 +463,18 @@ val make_abstract_instance : abstract_universe_context -> universe_instance
 
 (** {6 Pretty-printing of universes. } *)
 
-val pr_constraint_type : constraint_type -> Pp.std_ppcmds
-val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds
-val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds
-val pr_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> cumulativity_info -> Pp.std_ppcmds
-val pr_abstract_universe_context : (Level.t -> Pp.std_ppcmds) -> abstract_universe_context -> Pp.std_ppcmds
-val pr_abstract_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> abstract_cumulativity_info -> Pp.std_ppcmds
-val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds
-val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> 
-  univ_inconsistency -> Pp.std_ppcmds
-
-val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds
-val pr_universe_subst : universe_subst -> Pp.std_ppcmds
+val pr_constraint_type : constraint_type -> Pp.t
+val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t
+val pr_universe_context : (Level.t -> Pp.t) -> universe_context -> Pp.t
+val pr_cumulativity_info : (Level.t -> Pp.t) -> cumulativity_info -> Pp.t
+val pr_abstract_universe_context : (Level.t -> Pp.t) -> abstract_universe_context -> Pp.t
+val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> abstract_cumulativity_info -> Pp.t
+val pr_universe_context_set : (Level.t -> Pp.t) -> universe_context_set -> Pp.t
+val explain_universe_inconsistency : (Level.t -> Pp.t) -> 
+  univ_inconsistency -> Pp.t
+
+val pr_universe_level_subst : universe_level_subst -> Pp.t
+val pr_universe_subst : universe_subst -> Pp.t
 
 (** {6 Hash-consing } *)
 
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 6e9579aa4..df638acc1 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -50,9 +50,9 @@ type whd =
 
 (** For debugging purposes only *)
 
-val pr_atom : atom -> Pp.std_ppcmds
-val pr_whd : whd -> Pp.std_ppcmds
-val pr_stack : stack -> Pp.std_ppcmds
+val pr_atom : atom -> Pp.t
+val pr_whd : whd -> Pp.t
+val pr_stack : stack -> Pp.t
 
 (** Constructors *)