diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index d7b9516ae..aa5313842 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -369,7 +369,7 @@ module Hdir = Hashcons.Make( struct type t = dir_path type u = identifier -> identifier - let hash_sub hident d = list_smartmap hident d + let hash_sub hident d = List.smartmap hident d let rec equal d1 d2 = (d1==d2) || match (d1,d2) with |