aboutsummaryrefslogtreecommitdiff
path: root/kernel/mod_subst.ml
diff options
context:
space:
mode:
authorppedrot2012-10-29 13:02:23 +0000
committerppedrot2012-10-29 13:02:23 +0000
commit278517722988d040cb8da822e319d723670ac519 (patch)
tree92316184aec004570c6567f0d585167e47dd52ae /kernel/mod_subst.ml
parent0699ef2ffba984e7b7552787894b142dd924f66a (diff)
Removed many calls to OCaml generic equality. This was done by
writing our own comparison functions, and enforcing monomorphization in many places. This should be more efficient, btw. Still a work in progress. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/mod_subst.ml')
-rw-r--r--kernel/mod_subst.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 8bd0a653c9..f2511dbde6 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -50,7 +50,7 @@ let empty_delta_resolver = Deltamap.empty
module MBImap = Map.Make
(struct
type t = mod_bound_id
- let compare = Pervasives.compare
+ let compare = mod_bound_id_ord
end)
module Umap = struct