GitLab

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.