Skip to content
Snippets Groups Projects

solve_ndisj: try harder

Merged Ralf Jung requested to merge ralf/solve_ndisj into master
1 file
+ 1
1
Compare changes
  • Side-by-side
  • Inline
+ 1
1
@@ -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.
Loading