aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-03-30 13:19:45 +0200
committerGaëtan Gilbert2020-03-30 13:19:45 +0200
commit64e65e9fe7f0a4ea72ab195a4e8708a181c5abef (patch)
treeffb14c27988d3ead4d795d471d7a39191baf2823 /pretyping
parente21aae1b32adba4e8673783f327826d279e05ced (diff)
parentf3fb2f21646f257c0dd030a8411bafd80ea9d0bd (diff)
Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creation
Reviewed-by: SkySkimmer Reviewed-by: herbelin Ack-by: ppedrot
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercionops.ml12
1 files changed, 5 insertions, 7 deletions
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index d6458e1409..49401a9937 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -67,8 +67,6 @@ end
module ClTypMap = Map.Make(ClTyp)
-module IntMap = Map.Make(Int)
-
let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
type inheritance_path = coe_info_typ list
@@ -97,13 +95,13 @@ struct
module Index = struct include Int let print = Pp.int end
- type 'a t = { v : (cl_typ * 'a) IntMap.t; s : int; inv : int ClTypMap.t }
- let empty = { v = IntMap.empty; s = 0; inv = ClTypMap.empty }
+ type 'a t = { v : (cl_typ * 'a) Int.Map.t; s : int; inv : int ClTypMap.t }
+ let empty = { v = Int.Map.empty; s = 0; inv = ClTypMap.empty }
let mem y b = ClTypMap.mem y b.inv
- let map x b = IntMap.find x b.v
- let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (IntMap.find n b.v))
+ let map x b = Int.Map.find x b.v
+ let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v))
let add x y b =
- { v = IntMap.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
+ { v = Int.Map.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv [])
end