Make coPset operations TC opaque

See !108 (diffs, comment 43736)

This would be consistent with other set implementations.

mentioned in merge request !108 (merged)

This issue might apply to other set implementations, not just coPset. Off the top of my head:

• some set implementations make only elem_of opaque (e.g., mapset)

• the type gset is opaque but its operations are not (though gset_empty uses mapset_empty and the opaque gmap_empty)

The current situation is a total mess.

• For propset all operations are Global Opaque. For boolset ∈ is Typeclasses Opaque, some other operations are Global Opaque.
• For listset singleton and empty are Global Opaque.
• For gmultiset the operations are Typeclasses Opaque.
• For mapset only ∈ is opaque, and mapset_eq_dec is simpl never.

For hashset and listset_nodup (which are pretty much unused) there are yet other arbitrary choices.

I think the situation is as follows:

• Type class search should never unfold any of the set operations, so all of them should be Typeclasses Opaque.
• This does not affect simpl, so we used simpl never at few places. However, since simpl is broken beyond repair, we sometimes use Global Opaque (note that Opaque is Local by default) to make sure simpl really does not simplify.

So, maybe it's best to make all operations both Typeclasses Opaque and Global Opaque?

Making the set operations both Typeclasses Opaque and Global Opaque sounds reasonable to me.

It makes sense to document, somewhere in the source, the reason for Global Opaque, including a pointer to the closed simpl bug. In base.v alongside the set axioms and the Dom TC?