diff options
| author | Pierre-Marie Pédrot | 2020-09-22 18:36:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:21:14 +0200 |
| commit | 0a46af10ffc38726207bca952775102d48ad3b15 (patch) | |
| tree | 03ca56bb87e50a5d33c29183f74058fc99302735 /kernel/names.ml | |
| parent | 0590764209dcb8540b5292aca38fe2df38b90ab9 (diff) | |
Rename the GlobRef comparison modules following the standard pattern.
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 5f2ecea5f0..f7658df355 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -991,7 +991,7 @@ module GlobRef = struct (* By default, [global_reference] are ordered on their canonical part *) - module Ordered = struct + module CanOrd = struct open Constant.CanOrd type t = GlobRefInternal.t let compare gr1 gr2 = @@ -1000,7 +1000,7 @@ module GlobRef = struct let hash gr = GlobRefInternal.global_hash_gen hash ind_hash constructor_hash gr end - module Ordered_env = struct + module UserOrd = struct open Constant.UserOrd type t = GlobRefInternal.t let compare gr1 gr2 = @@ -1010,12 +1010,12 @@ module GlobRef = struct let hash gr = GlobRefInternal.global_hash_gen hash ind_user_hash constructor_user_hash gr end - module Map = HMap.Make(Ordered) + module Map = HMap.Make(CanOrd) module Set = Map.Set (* Alternative sets and maps indexed by the user part of the kernel names *) - module Map_env = HMap.Make(Ordered_env) + module Map_env = HMap.Make(UserOrd) module Set_env = Map_env.Set end |