diff options
| author | Hugo Herbelin | 2018-12-05 18:29:14 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-01-06 19:48:59 +0100 |
| commit | be54b359035067a3dcbcf57630063116523c41dd (patch) | |
| tree | 0e9eeec7ad16688744d370644c81ec59923f9380 /kernel/names.ml | |
| parent | 3d7eb01d428c9d98b10004f3f4f40b2209232971 (diff) | |
Documenting the internal role of to_string and print in Names.
In passing, slightly unify the API to make it clearer.
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 2 |
1 files changed, 2 insertions, 0 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 |