diff options
| author | Guillaume Melquiond | 2017-08-22 10:38:21 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2017-08-22 10:38:21 +0200 |
| commit | bd3a48926a075296486c552ccef6b87e3fddd5e4 (patch) | |
| tree | 4078ab1d058b1f045c880a2ac2d7091e6bd2c833 /lib/cArray.ml | |
| parent | 325890a83a2b073d9654b5615c585cd65a376fbd (diff) | |
Prevent overallocation in Array.map_to_list and remove custom implementation from Detyping.
Diffstat (limited to 'lib/cArray.ml')
| -rw-r--r-- | lib/cArray.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/lib/cArray.ml b/lib/cArray.ml index bb1e335468..85984d4362 100644 --- a/lib/cArray.ml +++ b/lib/cArray.ml @@ -283,8 +283,7 @@ let rev_of_list = function let () = set (len - 1) l in ans -let map_to_list f v = - List.map f (Array.to_list v) +let map_to_list = CList.map_of_array let map_of_list f l = let len = List.length l in |