diff options
Diffstat (limited to 'kernel/names.mli')
-rw-r--r-- | kernel/names.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 7cc444375..77139f1c3 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -217,6 +217,9 @@ sig 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]) *) @@ -244,6 +247,10 @@ sig (** Display *) val to_string : t -> string + + val debug_to_string : t -> string + (** Same as [to_string], but outputs information related to debug. *) + val print : t -> Pp.std_ppcmds (** Comparisons *) |