Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead

9 files changed, 19 insertions, 20 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 078990a8c..1cc072a2a 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -89,7 +89,7 @@ sig
     type t
     val compare : t -> t -> int
     val equal : t -> t -> bool
-    val print : t -> std_ppcmds
+    val print : t -> Pp.t
   end
   type 'a t
   val empty : 'a t
@@ -324,7 +324,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx;
 (* rajouter une coercion dans le graphe *)
 
 let path_printer = ref (fun _ -> str "<a class path>"
-                        : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> std_ppcmds)
+                        : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t)
 
 let install_path_printer f = path_printer := f
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 2e5ce30f3..8707078b5 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -95,15 +95,14 @@ val lookup_pattern_path_between :
 
 (**/**)
 (* Crade *)
-open Pp
 val install_path_printer :
-  ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit
+  ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
 (**/**)
 
 (** {6 This is for printing purpose } *)
 val string_of_class : cl_typ -> string
-val pr_class : cl_typ -> std_ppcmds
-val pr_cl_index : cl_index -> std_ppcmds
+val pr_class : cl_typ -> Pp.t
+val pr_cl_index : cl_index -> Pp.t
 val get_coercion_value : coe_index -> Constr.t
 val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
 val classes : unit -> cl_typ list
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f830d4be3..cac411183 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -81,7 +81,7 @@ let encode_tuple r =
 module PrintingInductiveMake =
   functor (Test : sig
      val encode : reference -> inductive
-     val member_message : std_ppcmds -> bool -> std_ppcmds
+     val member_message : Pp.t -> bool -> Pp.t
      val field : string
      val title : string
   end) ->
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index ffd67299d..59f3f967d 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -66,7 +66,7 @@ val subst_genarg_hook :
 module PrintingInductiveMake :
   functor (Test : sig
     val encode : Libnames.reference -> Names.inductive
-    val member_message : Pp.std_ppcmds -> bool -> Pp.std_ppcmds
+    val member_message : Pp.t -> bool -> Pp.t
     val field : string
     val title : string
   end) ->
@@ -75,9 +75,9 @@ module PrintingInductiveMake :
       val compare : t -> t -> int
       val encode : Libnames.reference -> Names.inductive
       val subst : substitution -> t -> t
-      val printer : t -> Pp.std_ppcmds
+      val printer : t -> Pp.t
       val key : Goptions.option_name
       val title : string
-      val member_message : t -> bool -> Pp.std_ppcmds
+      val member_message : t -> bool -> Pp.t
       val synchronous : bool
     end
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index c727332c7..5477c5c99 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -43,5 +43,5 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
 
 (** {6 debug pretty-printer:} *)
 
-val pr_tycon : env -> evar_map -> type_constraint -> Pp.std_ppcmds
+val pr_tycon : env -> evar_map -> type_constraint -> Pp.t
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index de09edcdc..5480b14af 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -67,7 +67,7 @@ type obj_typ = {
 (** Return the form of the component of a canonical structure *)
 val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list
 
-val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
+val pr_cs_pattern : cs_pattern -> Pp.t
 
 val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ
 val declare_canonical_structure : global_reference -> unit
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1d75fecb1..356323543 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -272,7 +272,7 @@ module Stack :
 sig
   open EConstr
   type 'a app_node
-  val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
+  val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
   type cst_member =
     | Cst_const of pconstant
@@ -290,7 +290,7 @@ sig
 
   exception IncompatibleFold2
 
-  val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+  val pr : ('a -> Pp.t) -> 'a t -> Pp.t
   val empty : 'a t
   val is_empty : 'a t -> bool
   val append_app : 'a array -> 'a t -> 'a t
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index db407b6c9..1828196fe 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -26,7 +26,7 @@ module ReductionBehaviour : sig
     bool -> Globnames.global_reference -> (int list * int * flag list) -> unit
   val get :
     Globnames.global_reference -> (int list * int * flag list) option
-  val print : Globnames.global_reference -> Pp.std_ppcmds
+  val print : Globnames.global_reference -> Pp.t
 end
 
 (** Option telling if reduction should use the refolding machinery of cbn
@@ -63,13 +63,13 @@ module Cst_stack : sig
   val best_cst : t -> (constr * constr list) option
   val best_replace : Evd.evar_map -> constr -> t -> constr -> constr
   val reference : Evd.evar_map -> t -> Constant.t option
-  val pr : t -> Pp.std_ppcmds
+  val pr : t -> Pp.t
 end
 
 module Stack : sig
   type 'a app_node
 
-  val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
+  val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
   type cst_member =
     | Cst_const of pconstant
@@ -86,7 +86,7 @@ module Stack : sig
   | Update of 'a
   and 'a t = 'a member list
 
-  val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+  val pr : ('a -> Pp.t) -> 'a t -> Pp.t
 
   val empty : 'a t
   val is_empty : 'a t -> bool
@@ -145,7 +145,7 @@ type contextual_state_reduction_function =
 type state_reduction_function = contextual_state_reduction_function
 type local_state_reduction_function = evar_map -> state -> state
 
-val pr_state : state -> Pp.std_ppcmds
+val pr_state : state -> Pp.t
 
 (** {6 Reduction Function Operators } *)
 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 163d3975a..ed3a9d0f9 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -48,4 +48,4 @@ val sorts_of_context : env -> evar_map -> rel_context -> sorts list
 
 val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
 
-val print_retype_error : retype_error -> Pp.std_ppcmds
+val print_retype_error : retype_error -> Pp.t