diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 6e39b35bb3..4466f558f9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -107,6 +107,7 @@ let label_of_mbid (_,s,_) = s let mk_label l = l let string_of_label = string_of_id +let pr_label l = str (string_of_label l) let id_of_label l = l let label_of_id id = id |