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

9 files changed, 22 insertions, 22 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 26c6e6014..9c69995f4 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -112,7 +112,7 @@ exception NotExtensibleClause
 val clenv_push_prod : clausenv -> clausenv
 
 (** {6 Pretty-print (debug only) } *)
-val pr_clenv : clausenv -> Pp.std_ppcmds
+val pr_clenv : clausenv -> Pp.t
 
 (** {6 Evar-based clauses} *)
 
diff --git a/proofs/goal.mli b/proofs/goal.mli
index cd71d11f8..6d3ec8bd4 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -20,7 +20,7 @@ val uid : goal -> string
 val get_by_uid : string -> goal
 
 (* Debugging help *)
-val pr_goal : goal -> Pp.std_ppcmds
+val pr_goal : goal -> Pp.t
 
 (* Layer to implement v8.2 tactic engine ontop of the new architecture. 
    Types are different from what they used to be due to a change of the
diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli
index 21d410c7b..b75718cd0 100644
--- a/proofs/miscprint.mli
+++ b/proofs/miscprint.mli
@@ -11,27 +11,27 @@ open Misctypes
 (** Printing of [intro_pattern] *)
 
 val pr_intro_pattern :
-  ('a -> Pp.std_ppcmds) -> 'a intro_pattern_expr Loc.located -> Pp.std_ppcmds
+  ('a -> Pp.t) -> 'a intro_pattern_expr Loc.located -> Pp.t
 
 val pr_or_and_intro_pattern :
-  ('a -> Pp.std_ppcmds) -> 'a or_and_intro_pattern_expr -> Pp.std_ppcmds
+  ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t
 
-val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds
+val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.t
 
 (** Printing of [move_location] *)
 
 val pr_move_location :
-  ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
+  ('a -> Pp.t) -> 'a move_location -> Pp.t
 
 val pr_bindings :
-  ('a -> Pp.std_ppcmds) ->
-  ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+  ('a -> Pp.t) ->
+  ('a -> Pp.t) -> 'a bindings -> Pp.t
 
 val pr_bindings_no_with :
-  ('a -> Pp.std_ppcmds) ->
-  ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds
+  ('a -> Pp.t) ->
+  ('a -> Pp.t) -> 'a bindings -> Pp.t
 
 val pr_with_bindings :
-  ('a -> Pp.std_ppcmds) ->
-  ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds
+  ('a -> Pp.t) ->
+  ('a -> Pp.t) -> 'a * 'a bindings -> Pp.t
 
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 1865382e4..698aa48b0 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -182,7 +182,7 @@ val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
    focused goals. *)
 val unshelve : proof -> proof
 
-val pr_proof : proof -> Pp.std_ppcmds
+val pr_proof : proof -> Pp.t
 
 (*** Compatibility layer with <=v8.2 ***)
 module V82 : sig
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index 9ae521d3f..9e924fec9 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -48,6 +48,6 @@ val suggest : proof -> Pp.t
 (*                                                        *)
 (**********************************************************)
 
-val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds
+val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t
 val get_default_goal_selector : unit -> Vernacexpr.goal_selector
 
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 20f5a0791..3b0a9e5b6 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -17,7 +17,7 @@ open Proofview
 
 (** Printer used to print the constr which refine refines. *)
 val pr_constr :
-  (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t
+  (Environ.env -> Evd.evar_map -> Term.constr -> Pp.t) Hook.t
 
 (** {7 Refinement primitives} *)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index f1b1cd359..3e3313eb5 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -63,7 +63,7 @@ let tclIDTAC_MESSAGE s gls =
 let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s)
 
 (* A special exception for levels for the Fail tactic *)
-exception FailError of int * std_ppcmds Lazy.t
+exception FailError of int * Pp.t Lazy.t
 
 (* The Fail tactic *)
 let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index aac10e81b..3ff010fe3 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -31,7 +31,7 @@ val refiner : rule -> tactic
 
 (** [tclIDTAC] is the identity tactic without message printing*)
 val tclIDTAC          : tactic
-val tclIDTAC_MESSAGE  : Pp.std_ppcmds -> tactic
+val tclIDTAC_MESSAGE  : Pp.t -> tactic
 
 (** [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
@@ -100,7 +100,7 @@ val tclTHENLASTn    : tactic -> tactic array -> tactic
 val tclTHENFIRSTn   : tactic -> tactic array -> tactic
 
 (** A special exception for levels for the Fail tactic *)
-exception FailError of int * Pp.std_ppcmds Lazy.t
+exception FailError of int * Pp.t Lazy.t
 
 (** Takes an exception and either raise it at the next
    level or do nothing. *)
@@ -116,8 +116,8 @@ val tclTRY           : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclCOMPLETE      : tactic -> tactic
 val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL          : int -> Pp.std_ppcmds -> tactic
-val tclFAIL_lazy     : int -> Pp.std_ppcmds Lazy.t -> tactic
+val tclFAIL          : int -> Pp.t -> tactic
+val tclFAIL_lazy     : int -> Pp.t Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclSHOWHYPS      : tactic -> tactic
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 2b7c36594..40b6573a1 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -94,8 +94,8 @@ val internal_cut_rev : bool -> Id.t -> types -> tactic
 val refine           : constr -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)
-val pr_gls    : goal sigma -> Pp.std_ppcmds
-val pr_glls   : goal list sigma -> Pp.std_ppcmds
+val pr_gls    : goal sigma -> Pp.t
+val pr_glls   : goal list sigma -> Pp.t
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig