aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/uGraph.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/uGraph.ml')
-rw-r--r--kernel/uGraph.ml16
1 files changed, 9 insertions, 7 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 4884d0deb..6971c0a2b 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -354,13 +354,15 @@ let get_new_edges g to_merge =
UMap.empty to_merge
in
let ltle =
- UMap.fold (fun _ n acc ->
- UMap.merge (fun _ strict1 strict2 ->
- match strict1, strict2 with
- | Some true, _ | _, Some true -> Some true
- | _, _ -> Some false)
- acc n.ltle)
- to_merge_lvl UMap.empty
+ let fold _ n acc =
+ let fold u strict acc =
+ if strict then UMap.add u strict acc
+ else if UMap.mem u acc then acc
+ else UMap.add u false acc
+ in
+ UMap.fold fold n.ltle acc
+ in
+ UMap.fold fold to_merge_lvl UMap.empty
in
let ltle, _ = clean_ltle g ltle in
let ltle =