Documenting the internal role of to_string and print in Names.

In passing, slightly unify the API to make it clearer.

2 files changed, 45 insertions, 17 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index b2d6a489a6..9f27212967 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -391,6 +391,8 @@ module KerName = struct
 
   let print kn = str (to_string kn)
 
+  let debug_print kn = str (debug_to_string kn)
+
   let compare (kn1 : kernel_name) (kn2 : kernel_name) =
     if kn1 == kn2 then 0
     else
diff --git a/kernel/names.mli b/kernel/names.mli
index 350db871d5..61df3bad0e 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -149,15 +149,15 @@ sig
   val is_empty : t -> bool
   (** Test whether a directory path is empty. *)
 
-  val to_string : t -> string
-  (** Print directory paths as ["coq_root.module.submodule"] *)
-
   val initial : t
   (** Initial "seed" of the unique identifier generator *)
 
   val hcons : t -> t
   (** Hashconsing of directory paths. *)
 
+  val to_string : t -> string
+  (** Print non-empty directory paths as ["coq_root.module.submodule"] *)
+
   val print : t -> Pp.t
 end
 
@@ -180,15 +180,15 @@ sig
   val make : string -> t
   (** Create a label out of a string. *)
 
-  val to_string : t -> string
-  (** Conversion to string. *)
-
   val of_id : Id.t -> t
   (** Conversion from an identifier. *)
 
   val to_id : t -> Id.t
   (** Conversion to an identifier. *)
 
+  val to_string : t -> string
+  (** Conversion to string. *)
+
   val print : t -> Pp.t
   (** Pretty-printer. *)
 
@@ -227,10 +227,10 @@ sig
   (** Return the identifier contained in the argument. *)
 
   val to_string : t -> string
-  (** Conversion to a string. *)
+  (** Encode as a string (not to be used for user-facing messages). *)
 
   val debug_to_string : t -> string
-  (** Same as [to_string], but outputs information related to debug. *)
+  (** Same as [to_string], but outputs extra information related to debug. *)
 
 end
 
@@ -252,16 +252,17 @@ sig
 
   val is_bound : t -> bool
 
-  val to_string : t -> string
-
-  val debug_to_string : t -> string
-  (** Same as [to_string], but outputs information related to debug. *)
-
   val initial : t
   (** Name of the toplevel structure ([= MPfile initial_dir]) *)
 
   val dp : t -> DirPath.t
 
+  val to_string : t -> string
+  (** Encode as a string (not to be used for user-facing messages). *)
+
+  val debug_to_string : t -> string
+  (** Same as [to_string], but outputs extra information related to debug. *)
+
 end
 
 module MPset : Set.S with type elt = ModPath.t
@@ -284,13 +285,17 @@ sig
   val modpath : t -> ModPath.t
   val label : t -> Label.t
 
-  (** Display *)
   val to_string : t -> string
+  (** Encode as a string (not to be used for user-facing messages). *)
+
+  val print : t -> Pp.t
+  (** Print internal representation (not to be used for user-facing messages). *)
 
   val debug_to_string : t -> string
-  (** Same as [to_string], but outputs information related to debug. *)
+  (** Same as [to_string], but outputs extra information related to debug. *)
 
-  val print : t -> Pp.t
+  val debug_print : t -> Pp.t
+  (** Same as [print], but outputs extra information related to debug. *)
 
   (** Comparisons *)
   val compare : t -> t -> int
@@ -365,9 +370,16 @@ sig
   (** Displaying *)
 
   val to_string : t -> string
+  (** Encode as a string (not to be used for user-facing messages). *)
+
   val print : t -> Pp.t
+  (** Print internal representation (not to be used for user-facing messages). *)
+
   val debug_to_string : t -> string
+  (** Same as [to_string], but outputs extra information related to debug. *)
+
   val debug_print : t -> Pp.t
+  (** Same as [print], but outputs extra information related to debug. *)
 
 end
 
@@ -444,9 +456,16 @@ sig
   (** Displaying *)
 
   val to_string : t -> string
+  (** Encode as a string (not to be used for user-facing messages). *)
+
   val print : t -> Pp.t
+  (** Print internal representation (not to be used for user-facing messages). *)
+
   val debug_to_string : t -> string
+  (** Same as [to_string], but outputs extra information related to debug. *)
+
   val debug_print : t -> Pp.t
+  (** Same as [print], but outputs extra information related to debug. *)
 
 end
 
@@ -567,8 +586,12 @@ module Projection : sig
     val map : (MutInd.t -> MutInd.t) -> t -> t
     val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t
 
-    val print : t -> Pp.t
     val to_string : t -> string
+    (** Encode as a string (not to be used for user-facing messages). *)
+
+    val print : t -> Pp.t
+    (** Print internal representation (not to be used for user-facing messages). *)
+
   end
   type t (* = Repr.t * bool *)
 
@@ -609,7 +632,10 @@ module Projection : sig
   val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t
 
   val to_string : t -> string
+  (** Encode as a string (not to be used for user-facing messages). *)
+
   val print : t -> Pp.t
+  (** Print internal representation (not to be used for user-facing messages). *)
 
 end