From e3c247c1d96f39d2c07d120b69598a904b7d9f19 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Sun, 11 Jun 2017 15:14:15 +0200 Subject: deprecate Pp.std_ppcmds type alias --- library/declaremods.mli | 2 +- library/goptions.ml | 10 +++++----- library/goptions.mli | 9 ++++----- library/keys.mli | 2 +- library/libnames.mli | 9 ++++----- library/nameops.mli | 8 ++++---- library/nametab.mli | 3 +-- 7 files changed, 20 insertions(+), 23 deletions(-) (limited to 'library') 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] -- cgit v1.2.3