Skip to content
Snippets Groups Projects
Commit 6c1d1ebf authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'ralf/solve_ndisj' into 'master'

solve_ndisj: try harder

See merge request robbertkrebbers/coq-stdpp!35
parents aa942ca8 a76a7ba7
No related branches found
No related tags found
1 merge request!35solve_ndisj: try harder
Pipeline #
......@@ -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.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment