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.

This should make theme asier to parse, "{{{ v, v; l |-> v }}}" looks rather funny.

Now we try to avoid adding them unnecessarily, so we don't have to remove them automatically any more.

There are now two proof mode tactics for dealing with modalities:

- `iModIntro` : introduction of a modality
- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality

The behavior of these tactics can be controlled by instances of the `IntroModal`
and `ElimModal` type class. We have declared instances for later, except 0,
basic updates and fancy updates. The tactic `iMod` is flexible enough that it
can also eliminate an updates around a weakest pre, and so forth.

The corresponding introduction patterns of these tactics are `!>` and `>`.

These tactics replace the tactics `iUpdIntro`, `iUpd` and `iTimeless`.

Source of backwards incompatability: the introduction pattern `!>` is used for
introduction of arbitrary modalities. It used to introduce laters by stripping
of a later of each hypotheses.

And also rename the corresponding proof mode tactics.

Before this commit, given "HP" : P and "H" : P -★ Q with Q persistent, one
could write:

  iSpecialize ("H" with "#HP")

to eliminate the wand in "H" while keeping the resource "HP". The lemma:

  own_valid : own γ x ⊢ ✓ x

was the prototypical example where this pattern (using the #) was used.

However, the pattern was too limited. For example, given "H" : P₁ -★ P₂ -★ Q",
one could not write iSpecialize ("H" with "#HP₁") because P₂ -★ Q is not
persistent, even when Q is.

So, instead, this commit introduces the following tactic:

  iSpecialize pm_trm as #

which allows one to eliminate implications and wands while being able to use
all hypotheses to prove the premises, as well as being able to use all
hypotheses to prove the resulting goal.

In the case of iDestruct, we now check whether all branches of the introduction
pattern start with an `#` (moving the hypothesis to the persistent context) or
`%` (moving the hypothesis to the pure Coq context). If this is the case, we
allow one to use all hypotheses for proving the premises, as well as for proving
the resulting goal.

I had to perform some renaming to avoid name clashes.

NB: these scopes delimiters were already there before Janno's a0067662.

This is more consistent with CAS, which also can be used on any value.
Note that being able to (atomically) test for equality of any value and
being able to CAS on any value is not realistic. See the discussion at
https://gitlab.mpi-sws.org/FP/iris-coq/issues/26, and in particular JH
Jourdan's observation:

  I think indeed for heap_lang this is just too complicated.

  Anyway, the role of heap_lang is not to model any actual
  programming language, but rather to show that we can do proofs
  about certain programs. The fact that you can write unrealistic
  programs is not a problem, IMHO. The only thing which is important
  is that the program that we write are realistic (i.e., faithfully
  represents the algorithm we want to p

This commit is based on a commit by Zhen Zhang who generalized equality
to work on any literal (and not just integers).