deprecate Pp.std_ppcmds type alias

1 files changed, 93 insertions, 94 deletions

diff --git a/printing/printer.mli b/printing/printer.mli
index f8685b089..2c9a4d70e 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Globnames
 open Term
@@ -25,96 +24,96 @@ val enable_goal_names_printing     : bool ref
 
 (** Terms *)
 
-val pr_lconstr_env         : env -> evar_map -> constr -> std_ppcmds
-val pr_lconstr             : constr -> std_ppcmds
-val pr_lconstr_goal_style_env : env -> evar_map -> constr -> std_ppcmds
+val pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
+val pr_lconstr             : constr -> Pp.t
+val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
-val pr_constr_env          : env -> evar_map -> constr -> std_ppcmds
-val pr_constr              : constr -> std_ppcmds
-val pr_constr_goal_style_env : env -> evar_map -> constr -> std_ppcmds
+val pr_constr_env          : env -> evar_map -> constr -> Pp.t
+val pr_constr              : constr -> Pp.t
+val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
 (** Same, but resilient to [Nametab] errors. Prints fully-qualified
     names when [shortest_qualid_of_global] has failed. Prints "??"
     in case of remaining issues (such as reference not in env). *)
 
-val safe_pr_lconstr_env         : env -> evar_map -> constr -> std_ppcmds
-val safe_pr_lconstr             : constr -> std_ppcmds
+val safe_pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
+val safe_pr_lconstr             : constr -> Pp.t
 
-val safe_pr_constr_env          : env -> evar_map -> constr -> std_ppcmds
-val safe_pr_constr              : constr -> std_ppcmds
+val safe_pr_constr_env          : env -> evar_map -> constr -> Pp.t
+val safe_pr_constr              : constr -> Pp.t
 
-val pr_econstr_env     : env -> evar_map -> EConstr.t -> std_ppcmds
-val pr_econstr         : EConstr.t -> std_ppcmds
-val pr_leconstr_env     : env -> evar_map -> EConstr.t -> std_ppcmds
-val pr_leconstr         : EConstr.t -> std_ppcmds
+val pr_econstr_env     : env -> evar_map -> EConstr.t -> Pp.t
+val pr_econstr         : EConstr.t -> Pp.t
+val pr_leconstr_env     : env -> evar_map -> EConstr.t -> Pp.t
+val pr_leconstr         : EConstr.t -> Pp.t
 
-val pr_etype_env           : env -> evar_map -> EConstr.types -> std_ppcmds
-val pr_letype_env           : env -> evar_map -> EConstr.types -> std_ppcmds
+val pr_etype_env           : env -> evar_map -> EConstr.types -> Pp.t
+val pr_letype_env           : env -> evar_map -> EConstr.types -> Pp.t
 
-val pr_open_constr_env     : env -> evar_map -> open_constr -> std_ppcmds
-val pr_open_constr         : open_constr -> std_ppcmds
+val pr_open_constr_env     : env -> evar_map -> open_constr -> Pp.t
+val pr_open_constr         : open_constr -> Pp.t
 
-val pr_open_lconstr_env    : env -> evar_map -> open_constr -> std_ppcmds
-val pr_open_lconstr        : open_constr -> std_ppcmds
+val pr_open_lconstr_env    : env -> evar_map -> open_constr -> Pp.t
+val pr_open_lconstr        : open_constr -> Pp.t
 
-val pr_constr_under_binders_env  : env -> evar_map -> constr_under_binders -> std_ppcmds
-val pr_constr_under_binders      : constr_under_binders -> std_ppcmds
+val pr_constr_under_binders_env  : env -> evar_map -> constr_under_binders -> Pp.t
+val pr_constr_under_binders      : constr_under_binders -> Pp.t
 
-val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds
-val pr_lconstr_under_binders     : constr_under_binders -> std_ppcmds
+val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t
+val pr_lconstr_under_binders     : constr_under_binders -> Pp.t
 
-val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> std_ppcmds
-val pr_ltype_env           : env -> evar_map -> types -> std_ppcmds
-val pr_ltype               : types -> std_ppcmds
+val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t
+val pr_ltype_env           : env -> evar_map -> types -> Pp.t
+val pr_ltype               : types -> Pp.t
 
-val pr_type_env            : env -> evar_map -> types -> std_ppcmds
-val pr_type                : types -> std_ppcmds
+val pr_type_env            : env -> evar_map -> types -> Pp.t
+val pr_type                : types -> Pp.t
 
-val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> std_ppcmds
-val pr_closed_glob         : closed_glob_constr -> std_ppcmds
+val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> Pp.t
+val pr_closed_glob         : closed_glob_constr -> Pp.t
 
-val pr_ljudge_env          : env -> evar_map -> EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds
-val pr_ljudge              : EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds
+val pr_ljudge_env          : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t
+val pr_ljudge              : EConstr.unsafe_judgment -> Pp.t * Pp.t
 
-val pr_lglob_constr_env      : env -> glob_constr -> std_ppcmds
-val pr_lglob_constr          : glob_constr -> std_ppcmds
+val pr_lglob_constr_env      : env -> glob_constr -> Pp.t
+val pr_lglob_constr          : glob_constr -> Pp.t
 
-val pr_glob_constr_env       : env -> glob_constr -> std_ppcmds
-val pr_glob_constr           : glob_constr -> std_ppcmds
+val pr_glob_constr_env       : env -> glob_constr -> Pp.t
+val pr_glob_constr           : glob_constr -> Pp.t
 
-val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> std_ppcmds
-val pr_lconstr_pattern     : constr_pattern -> std_ppcmds
+val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t
+val pr_lconstr_pattern     : constr_pattern -> Pp.t
 
-val pr_constr_pattern_env  : env -> evar_map -> constr_pattern -> std_ppcmds
-val pr_constr_pattern      : constr_pattern -> std_ppcmds
+val pr_constr_pattern_env  : env -> evar_map -> constr_pattern -> Pp.t
+val pr_constr_pattern      : constr_pattern -> Pp.t
 
-val pr_cases_pattern       : cases_pattern -> std_ppcmds
+val pr_cases_pattern       : cases_pattern -> Pp.t
 
-val pr_sort                : evar_map -> sorts -> std_ppcmds
+val pr_sort                : evar_map -> sorts -> Pp.t
 
 (** Universe constraints *)
 
-val pr_polymorphic         : bool -> std_ppcmds
-val pr_cumulative          : bool -> bool -> std_ppcmds
-val pr_universe_instance   : evar_map -> Univ.universe_context -> std_ppcmds
-val pr_universe_ctx        : evar_map -> Univ.universe_context -> std_ppcmds
-val pr_cumulativity_info   : evar_map -> Univ.cumulativity_info -> std_ppcmds
+val pr_polymorphic         : bool -> Pp.t
+val pr_cumulative          : bool -> bool -> Pp.t
+val pr_universe_instance   : evar_map -> Univ.universe_context -> Pp.t
+val pr_universe_ctx        : evar_map -> Univ.universe_context -> Pp.t
+val pr_cumulativity_info   : evar_map -> Univ.cumulativity_info -> Pp.t
 
 (** Printing global references using names as short as possible *)
 
-val pr_global_env          : Id.Set.t -> global_reference -> std_ppcmds
-val pr_global              : global_reference -> std_ppcmds
+val pr_global_env          : Id.Set.t -> global_reference -> Pp.t
+val pr_global              : global_reference -> Pp.t
 
-val pr_constant            : env -> constant -> std_ppcmds
-val pr_existential_key     : evar_map -> existential_key -> std_ppcmds
-val pr_existential         : env -> evar_map -> existential -> std_ppcmds
-val pr_constructor         : env -> constructor -> std_ppcmds
-val pr_inductive           : env -> inductive -> std_ppcmds
-val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds
+val pr_constant            : env -> constant -> Pp.t
+val pr_existential_key     : evar_map -> existential_key -> Pp.t
+val pr_existential         : env -> evar_map -> existential -> Pp.t
+val pr_constructor         : env -> constructor -> Pp.t
+val pr_inductive           : env -> inductive -> Pp.t
+val pr_evaluable_reference : evaluable_global_reference -> Pp.t
 
-val pr_pconstant           : env -> pconstant -> std_ppcmds
-val pr_pinductive          : env -> pinductive -> std_ppcmds
-val pr_pconstructor        : env -> pconstructor -> std_ppcmds
+val pr_pconstant           : env -> pconstant -> Pp.t
+val pr_pinductive          : env -> pinductive -> Pp.t
+val pr_pconstructor        : env -> pconstructor -> Pp.t
 
 
 (** Contexts *)
@@ -122,29 +121,29 @@ val pr_pconstructor        : env -> pconstructor -> std_ppcmds
 val set_compact_context : bool -> unit
 val get_compact_context : unit -> bool
 
-val pr_context_unlimited   : env -> evar_map -> std_ppcmds
-val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
+val pr_context_unlimited   : env -> evar_map -> Pp.t
+val pr_ne_context_of       : Pp.t -> env -> evar_map -> Pp.t
 
-val pr_named_decl          : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds
-val pr_compacted_decl      : env -> evar_map -> Context.Compacted.Declaration.t -> std_ppcmds
-val pr_rel_decl            : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds
+val pr_named_decl          : env -> evar_map -> Context.Named.Declaration.t -> Pp.t
+val pr_compacted_decl      : env -> evar_map -> Context.Compacted.Declaration.t -> Pp.t
+val pr_rel_decl            : env -> evar_map -> Context.Rel.Declaration.t -> Pp.t
 
-val pr_named_context       : env -> evar_map -> Context.Named.t -> std_ppcmds
-val pr_named_context_of    : env -> evar_map -> std_ppcmds
-val pr_rel_context         : env -> evar_map -> Context.Rel.t -> std_ppcmds
-val pr_rel_context_of      : env -> evar_map -> std_ppcmds
-val pr_context_of          : env -> evar_map -> std_ppcmds
+val pr_named_context       : env -> evar_map -> Context.Named.t -> Pp.t
+val pr_named_context_of    : env -> evar_map -> Pp.t
+val pr_rel_context         : env -> evar_map -> Context.Rel.t -> Pp.t
+val pr_rel_context_of      : env -> evar_map -> Pp.t
+val pr_context_of          : env -> evar_map -> Pp.t
 
 (** Predicates *)
 
-val pr_predicate           : ('a -> std_ppcmds) -> (bool * 'a list) -> std_ppcmds
-val pr_cpred               : Cpred.t -> std_ppcmds
-val pr_idpred              : Id.Pred.t -> std_ppcmds
-val pr_transparent_state   : transparent_state -> std_ppcmds
+val pr_predicate           : ('a -> Pp.t) -> (bool * 'a list) -> Pp.t
+val pr_cpred               : Cpred.t -> Pp.t
+val pr_idpred              : Id.Pred.t -> Pp.t
+val pr_transparent_state   : transparent_state -> Pp.t
 
 (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
 
-val pr_goal                : goal sigma -> std_ppcmds
+val pr_goal                : goal sigma -> Pp.t
 
 (** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals]
    prints the goals of the list [goals] followed by the goals in
@@ -155,25 +154,25 @@ val pr_goal                : goal sigma -> std_ppcmds
    focused goals unless the conrresponding option
    [enable_unfocused_goal_printing] is set. [seeds] is for printing
    dependent evars (mainly for emacs proof tree mode). *)
-val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list
-                             -> goal list -> goal list -> std_ppcmds
+val pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list
+                             -> goal list -> goal list -> Pp.t
 
-val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
-val pr_concl               : int -> evar_map -> goal -> std_ppcmds
+val pr_subgoal             : int -> evar_map -> goal list -> Pp.t
+val pr_concl               : int -> evar_map -> goal -> Pp.t
 
-val pr_open_subgoals       : ?proof:Proof.proof -> unit -> std_ppcmds
-val pr_nth_open_subgoal    : int -> std_ppcmds
-val pr_evar                : evar_map -> (evar * evar_info) -> std_ppcmds
-val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds
-val pr_evars               : evar_map -> evar_info Evar.Map.t -> std_ppcmds
-val pr_ne_evar_set         : std_ppcmds -> std_ppcmds -> evar_map ->
-  Evar.Set.t -> std_ppcmds
+val pr_open_subgoals       : ?proof:Proof.proof -> unit -> Pp.t
+val pr_nth_open_subgoal    : int -> Pp.t
+val pr_evar                : evar_map -> (evar * evar_info) -> Pp.t
+val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> Pp.t
+val pr_evars               : evar_map -> evar_info Evar.Map.t -> Pp.t
+val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
+  Evar.Set.t -> Pp.t
 
-val pr_prim_rule           : prim_rule -> std_ppcmds
+val pr_prim_rule           : prim_rule -> Pp.t
 
 (** Backwards compatibility *)
 
-val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
+val prterm                 : constr -> Pp.t (** = pr_lconstr *)
 
 
 (** Declarations for the "Print Assumption" command *)
@@ -193,15 +192,15 @@ module ContextObjectMap : CMap.ExtS
   with type key = context_object and module Set := ContextObjectSet
 
 val pr_assumptionset :
-  env -> Term.types ContextObjectMap.t -> std_ppcmds
+  env -> Term.types ContextObjectMap.t -> Pp.t
 
-val pr_goal_by_id : Id.t -> std_ppcmds
-val pr_goal_by_uid : string -> std_ppcmds
+val pr_goal_by_id : Id.t -> Pp.t
+val pr_goal_by_uid : string -> Pp.t
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds;
- pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
- pr_goal                : goal sigma -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
+ pr_subgoal             : int -> evar_map -> goal list -> Pp.t;
+ pr_goal                : goal sigma -> Pp.t;
 };;
 
 val set_printer_pr : printer_pr -> unit