Also, higher cost for [elim_modal_bupd_fupd], so that it is not taken in place of [elim_modal_fupd_fupd] in spec patterns.

No longer `put box_own_prop γ P` in the invariant, it is persistent.

    The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.

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.

Use COFEs only for the recursive domain equation solver

In particular, make sure we always try eassumption before reflexivity.

The old name didn't make much sense. Also now we can have
pure_False too.

We need instances like EqDecision and Countable for it. We could
redeclare those instead, though.

There is no way to infer the cmra A, so we make it explicit.

The old choice for ★ was a arbitrary: the precedence of the ASCII asterisk *
was fixed at a wrong level in Coq, so we had to pick another symbol. The ★ was
a random choice from a unicode chart.

The new symbol ∗ (as proposed by David Swasey) corresponds better to
conventional practise and matches the symbol we use on paper.