diff options
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 |