fix(th-data): avoid redundant explanations

This commit is contained in:
Simon Cruanes 2019-12-28 09:00:59 -06:00
parent e58b29da02
commit 10b9febe9d

View file

@ -170,7 +170,6 @@ module Make(A : ARG) : S with module A = A = struct
Expl.mk_list [ Expl.mk_list [
Expl.mk_merge n1 c1.c_n; Expl.mk_merge n1 c1.c_n;
Expl.mk_merge n2 c2.c_n; Expl.mk_merge n2 c2.c_n;
Expl.mk_merge n1 n2;
] ]
in in
if A.Cstor.equal c1.c_cstor c2.c_cstor then ( if A.Cstor.equal c1.c_cstor c2.c_cstor then (