It now first turns hypotheses `X ∪ Y ⊆ Z` into `X ⊆ Z` and `Y ⊆ Z`.

This approach is originally by Robbert

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

Robbert Krebbers authored 8 years ago and Ralf Jung committed 8 years ago

We do this by introducing a type class UpClose with notation ↑.

The reason for this change is as follows: since `nclose : namespace
→ coPset` is declared as a coercion, the notation `nclose N ⊆ E` was
pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked
because type checking goes from left to right, and as such would look
for an instance `SubsetEq namespace`, which causes the right hand side
to be ill-typed.

Define disjointness of namespaces in terms of masks.\n\nThe proofs are made simpler and some lemmas get more general.

This way we ensure that Coq gives an error message when one accidentially
writes "N ⊆ E" instead of "nclose N ⊆ E". Before, it used the ⊆ instance of
lists.

Similar files (gmap, listset, ...) were already in singular form and
matched the name of the set/map data type.

Both ndot and nclose involve encodings of countable types, and conversion
should thus never unfold these definitions.

In particular, it no longer uses set_solver (which made it often slow
or diverge) but a more specific lemma about subseteq.

Thanks to Amin Timany for the suggestion.

It now traverses terms at most once, whereas the setoid_rewrite
approach was travering terms many times. Also, the tactic can now
be extended by defining type class instances.

The non applied one should be only parsing.