diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 6ee96fddd5..953c13aa95 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -51,13 +51,7 @@ type name = Name of identifier | Anonymous type module_ident = identifier type dir_path = module_ident list -module ModIdOrdered = - struct - type t = identifier - let compare = Pervasives.compare - end - -module ModIdmap = Map.Make(ModIdOrdered) +module ModIdmap = Idmap let make_dirpath x = x let repr_dirpath x = x |