diff options
| author | Maxime Dénès | 2017-08-31 11:51:38 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-31 11:51:38 +0200 |
| commit | 8f04b4714f2a797b98be4d87866af3d93ecb78b6 (patch) | |
| tree | 492e08d1f445fbc62476540dfbe1de4bdb01ea20 /lib/cArray.ml | |
| parent | 2c50427e59f932f26a8b643ea30c158c5deb432a (diff) | |
| parent | bd3a48926a075296486c552ccef6b87e3fddd5e4 (diff) | |
Merge PR #989: 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 |