deprecate Pp.std_ppcmds type alias

7 files changed, 20 insertions, 23 deletions

diff --git a/library/declaremods.mli b/library/declaremods.mli
index 1f2aaf7b5..005594b8d 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -121,7 +121,7 @@ val iter_all_segments :
   (Libnames.object_name -> Libobject.obj -> unit) -> unit
 
 
-val debug_print_modtab : unit -> Pp.std_ppcmds
+val debug_print_modtab : unit -> Pp.t
 
 (** For printing modules, [process_module_binding] adds names of
     bound module (and its components) to Nametab. It also loads
diff --git a/library/goptions.ml b/library/goptions.ml
index fe014ef68..184c6fa11 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -57,10 +57,10 @@ module MakeTable =
 	  val table : (string * key table_of_A) list ref
 	  val encode : key -> t
 	  val subst : substitution -> t -> t
-          val printer : t -> std_ppcmds
+          val printer : t -> Pp.t
           val key : option_name
           val title : string
-          val member_message : t -> bool -> std_ppcmds
+          val member_message : t -> bool -> Pp.t
         end) ->
   struct
     type option_mark =
@@ -131,7 +131,7 @@ module type StringConvertArg =
 sig
   val key : option_name
   val title : string
-  val member_message : string -> bool -> std_ppcmds
+  val member_message : string -> bool -> Pp.t
 end
 
 module StringConvert = functor (A : StringConvertArg) ->
@@ -161,10 +161,10 @@ sig
   val compare : t -> t -> int
   val encode : reference -> t
   val subst : substitution -> t -> t
-  val printer : t -> std_ppcmds
+  val printer : t -> Pp.t
   val key : option_name
   val title : string
-  val member_message : t -> bool -> std_ppcmds
+  val member_message : t -> bool -> Pp.t
 end
 
 module RefConvert = functor (A : RefConvertArg) ->
diff --git a/library/goptions.mli b/library/goptions.mli
index 3100c1ce7..cec7250f1 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -43,7 +43,6 @@
    All options are synchronized with the document.
 *)
 
-open Pp
 open Libnames
 open Mod_subst
 
@@ -64,7 +63,7 @@ module MakeStringTable :
     (A : sig
        val key : option_name
        val title : string
-       val member_message : string -> bool -> std_ppcmds
+       val member_message : string -> bool -> Pp.t
      end) ->
 sig
   val active : string -> bool
@@ -88,10 +87,10 @@ module MakeRefTable :
            val compare : t -> t -> int
            val encode : reference -> t
 	   val subst : substitution -> t -> t
-           val printer : t -> std_ppcmds
+           val printer : t -> Pp.t
            val key : option_name
            val title : string
-           val member_message : t -> bool -> std_ppcmds
+           val member_message : t -> bool -> Pp.t
          end) ->
     sig
       val active : A.t -> bool
@@ -177,6 +176,6 @@ type option_state = {
 }
 
 val get_tables : unit -> option_state OptionMap.t
-val print_tables : unit -> std_ppcmds
+val print_tables : unit -> Pp.t
 
 val error_undeclared_key : option_name -> 'a
diff --git a/library/keys.mli b/library/keys.mli
index 6fe9efc6e..d5dc0e2a1 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -19,5 +19,5 @@ val equiv_keys : key -> key -> bool
 val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
 (** Compute the head key of a term. *)
 
-val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds
+val pr_keys : (global_reference -> Pp.t) -> Pp.t
 (** Pretty-print the mapping *)
diff --git a/library/libnames.mli b/library/libnames.mli
index b6d6f7f3b..1b351290a 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -7,14 +7,13 @@
 (************************************************************************)
 
 open Util
-open Pp
 open Loc
 open Names
 
 (** {6 Dirpaths } *)
 (** FIXME: ought to be in Names.dir_path *)
 
-val pr_dirpath : DirPath.t -> Pp.std_ppcmds
+val pr_dirpath : DirPath.t -> Pp.t
 
 val dirpath_of_string : string -> DirPath.t
 val string_of_dirpath : DirPath.t -> string
@@ -58,7 +57,7 @@ val basename : full_path -> Id.t
 (** Parsing and printing of section path as ["coq_root.module.id"] *)
 val path_of_string : string -> full_path
 val string_of_path : full_path -> string
-val pr_path : full_path -> std_ppcmds
+val pr_path : full_path -> Pp.t
 
 module Spmap  : CSig.MapS with type key = full_path
 
@@ -77,7 +76,7 @@ val repr_qualid : qualid -> DirPath.t * Id.t
 
 val qualid_eq : qualid -> qualid -> bool
 
-val pr_qualid : qualid -> std_ppcmds
+val pr_qualid : qualid -> Pp.t
 val string_of_qualid : qualid -> string
 val qualid_of_string : string -> qualid
 
@@ -124,7 +123,7 @@ type reference =
 val eq_reference : reference -> reference -> bool
 val qualid_of_reference : reference -> qualid located
 val string_of_reference : reference -> string
-val pr_reference : reference -> std_ppcmds
+val pr_reference : reference -> Pp.t
 val loc_of_reference : reference -> Loc.t option
 val join_reference : reference -> reference -> reference
 
diff --git a/library/nameops.mli b/library/nameops.mli
index 88290f485..89aba2447 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -106,13 +106,13 @@ val name_max : Name.t -> Name.t -> Name.t
 val name_cons : Name.t -> Id.t list -> Id.t list
 (** @deprecated Same as [Name.cons] *)
 
-val pr_name : Name.t -> Pp.std_ppcmds
+val pr_name : Name.t -> Pp.t
 (** @deprecated Same as [Name.print] *)
 
-val pr_id : Id.t -> Pp.std_ppcmds
+val pr_id : Id.t -> Pp.t
 (** @deprecated Same as [Names.Id.print] *)
 
-val pr_lab : Label.t -> Pp.std_ppcmds
+val pr_lab : Label.t -> Pp.t
 
 (** some preset paths *)
 
@@ -127,5 +127,5 @@ val coq_string : string (** "Coq" *)
 val default_root_prefix : DirPath.t
 
 (** Metavariables *)
-val pr_meta : Term.metavariable -> Pp.std_ppcmds
+val pr_meta : Term.metavariable -> Pp.t
 val string_of_meta : Term.metavariable -> string
diff --git a/library/nametab.mli b/library/nametab.mli
index be57f5dcc..025a63b1c 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Libnames
 open Globnames
@@ -155,7 +154,7 @@ val basename_of_global : global_reference -> Id.t
 
 (** Printing of global references using names as short as possible.
     @raise Not_found when the reference is not in the global tables. *)
-val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds
+val pr_global_env : Id.Set.t -> global_reference -> Pp.t
 
 
 (** The [shortest_qualid] functions given an object with [user_name]