aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/merge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/merge.ml')
-rw-r--r--plugins/funind/merge.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 30c60b52b..2c44353f2 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -663,9 +663,9 @@ let build_link_map_aux (allargs1:Id.t array) (allargs2:Id.t array)
let build_link_map allargs1 allargs2 lnk =
let allargs1 =
- Array.of_list (List.rev (List.map (fun (x,_,_) -> id_of_name x) allargs1)) in
+ Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs1) in
let allargs2 =
- Array.of_list (List.rev (List.map (fun (x,_,_) -> id_of_name x) allargs2)) in
+ Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs2) in
build_link_map_aux allargs1 allargs2 lnk