Commit a76a7ba7 authored by Ralf Jung's avatar Ralf Jung

solve_ndisj: try harder

parent aa942ca8
......@@ -101,5 +101,5 @@ Ltac solve_ndisj :=
repeat match goal with
| H : _ _ _ |- _ => apply union_subseteq in H as [??]
end;
solve [eauto with ndisj].
solve [eauto 10 with ndisj].
Hint Extern 1000 => solve_ndisj : solve_ndisj.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment