diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Collections.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Collections.ml b/src/Collections.ml index 80345e14..bb7c37f1 100644 --- a/src/Collections.ml +++ b/src/Collections.ml @@ -193,7 +193,7 @@ end identifiers to names (i.e., strings) when generating code, in order to make sure that we don't have potentially dangerous collisions. *) -module type MapInj = sig +module type InjMap = sig type key type elem @@ -271,9 +271,9 @@ module type MapInj = sig val of_list : (key * elem) list -> t end -(** See [MapInj] *) -module MakeMapInj (Key : OrderedType) (Elem : OrderedType) : - MapInj with type key = Key.t with type elem = Elem.t = struct +(** See [InjMap] *) +module MakeInjMap (Key : OrderedType) (Elem : OrderedType) : + InjMap with type key = Key.t with type elem = Elem.t = struct module Map = MakeMap (Key) module Set = MakeSet (Elem) |