diff options
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 2d112b32ac..acc764028f 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -47,6 +47,7 @@ type label val mk_label : string -> label val string_of_label : label -> string +val pr_label : label -> Pp.std_ppcmds val label_of_id : identifier -> label val id_of_label : label -> identifier |