move coPset-generic hint to coPset.v

I see no good reason for it to be in namespaces.v. The old one that got removed in e09f7ce3 was in coPset.v as well.

I presume the more general Hint Resolve top_subseteq : core simply won't help with the regression that forced the switch from ndisj to core.

So this looks good to me.

I'm fine moving it here. But can we at least have a comment why we need this hint (namely that it's used for ndisj and comes up often in Iris).

mentioned in commit 1f223f8f

added 1 commit

• 829dc991 - add comment

Compare with previous version

resolved all threads

merged

mentioned in commit f84c69f6

LGTM.

mentioned in commit e0eef94a