aboutsummaryrefslogtreecommitdiffstats
path: root/lib/UnionFind.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/UnionFind.v')
-rw-r--r--lib/UnionFind.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index 27278b01..20bb91cd 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.v
@@ -422,7 +422,7 @@ Definition merge (uf: t) (a b: elt) : t :=
let b' := repr uf b in
match M.elt_eq a' b' with
| left EQ => uf
- | right NEQ => identify uf a' b (repr_res_none uf a) (sym_not_equal NEQ)
+ | right NEQ => identify uf a' b (repr_res_none uf a) (not_eq_sym NEQ)
end.
Lemma repr_merge: