diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-08 02:44:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-08 17:40:23 +0100 |
| commit | 643e624909ecec7ba43326ff962b13c184991125 (patch) | |
| tree | efb6eb90e799f0322917103151a6185565de23c2 /kernel/names.ml | |
| parent | adcc15063fd917e7c93ee73cf43b15b667f98742 (diff) | |
Using HMaps in global references.
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 50402eb83..6b433c482 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -561,6 +561,8 @@ let ind_user_ord (m1, i1) (m2, i2) = if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c let ind_hash (m, i) = Hashset.Combine.combine (MutInd.hash m) (Int.hash i) +let ind_user_hash (m, i) = + Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i) let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 let constructor_ord (ind1, j1) (ind2, j2) = @@ -571,6 +573,8 @@ let constructor_user_ord (ind1, j1) (ind2, j2) = if Int.equal c 0 then ind_user_ord ind1 ind2 else c let constructor_hash (ind, i) = Hashset.Combine.combine (ind_hash ind) (Int.hash i) +let constructor_user_hash (ind, i) = + Hashset.Combine.combine (ind_user_hash ind) (Int.hash i) module InductiveOrdered = struct type t = inductive |