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.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index a811b29b8..485b5b280 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -227,7 +227,7 @@ let linkmonad f lnkvar =
let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar
(* This map is used to deal with debruijn linked indices. *)
-module Link = Map.Make (struct type t = int let compare = Pervasives.compare end)
+module Link = Map.Make (Int)
let pr_links l =
Printf.printf "links:\n";