Also make those for introduction and elimination more symmetric:

  !%   pure introduction         %        pure elimination
  !#   always introduction       #        always elimination
  !>   later introduction        > pat    timeless later elimination
  !==> view shift introduction   ==> pat  view shift elimination

This commit features:

- A simpler model. The recursive domain equation no longer involves a triple
  containing invariants, physical state and ghost state, but just ghost state.
  Invariants and physical state are encoded using (higher-order) ghost state.

- (Primitive) view shifts are formalized in the logic and all properties about
  it are proven in the logic instead of the model. Instead, the core logic
  features only a notion of raw view shifts which internalizing performing frame
  preserving updates.

- A better behaved notion of mask changing view shifts. In particular, we no
  longer have side-conditions on transitivity of view shifts, and we have a
  rule for introduction of mask changing view shifts |={E1,E2}=> P with
  E2 ⊆ E1 which allows to postpone performing a view shift.

- The weakest precondition connective is formalized in the logic using Banach's
  fixpoint. All properties about the connective are proven in the logic instead
  of directly in the model.

- Adequacy is proven in the logic and uses a primitive form of adequacy for
  uPred that only involves raw views shifts and laters.

Some remarks:

- I have removed binary view shifts. I did not see a way to describe all rules
  of the new mask changing view shifts using those.
- There is no longer the need for the notion of "frame shifting assertions" and
  these are thus removed. The rules for Hoare triples are thus also stated in
  terms of primitive view shifts.

TODO:

- Maybe rename primitive view shift into something more sensible
- Figure out a way to deal with closed proofs (see the commented out stuff in
  tests/heap_lang and tests/barrier_client).

This avoids recompilation of coq_tactics each time an instance is added.

The new implementation ensures that type class arguments are only infered
in the very end. This avoids the need for the inG hack in a0348d7c.

This reverts commit c43eb936.

The hack using class_apply has some strange behaviors, see:

  https://sympa.inria.fr/sympa/arc/coq-club/2016-07/msg00094.html

The intropattern {H} also meant clear (both in ssreflect, and the logic
part of the introduction pattern).

For example iIntros "{$H1 H2} H1" frames H1, clears H2, and introduces H1.

This fixes a bug in 916ff44a causing proof mode notations not being
pretty printed.

This tweak allows us to declare pvs as an instance of FromPure (it is not
an instance of IntoPure), making some tactics (like iPureIntro and done)
work with pvs too.

We are now using the prefixes Into, From, and Is (the first two are
inspired by the names of some traits in the Rust stdlib), and hopefully
doing that consistenly.

This introduces n hypotheses and destructs the nth one.

Generating a fresh name consists of two stages:
+ Use [cbv] to compute a list representing the domain of the environment. This
  is a very simply computation that just erases the hypotheses.
+ Use [vm_compute] to compute a fresh name based on the list representing the
  domain. The domain itself should never contain evars, so [vm_compute] will
  do the job.

To do so, we have introduced the specialization patterns:

  =>[H1 .. Hn] and =>[-H1 .. Hn]

That generate a goal in which the view shift is preserved. These specialization
patterns can also be used for e.g. iApply.

Note that this machinery is not tied to primitive view shifts, and works for
various kinds of goal (as captured by the ToAssert type class, which describes
how to transform the asserted goal based on the main goal).

TODO: change the name of these specialization patterns to reflect this
generality.

Changes:
- We no longer have a different syntax for specializing a term H : P -★ Q whose
  range P or domain Q is persistent. There is just one syntax, and the system
  automatically determines whether either P or Q is persistent.
- While specializing a term, always modalities are automatically stripped. This
  gets rid of the specialization pattern !.
- Make the syntax of specialization patterns more consistent. The syntax for
  generating a goal is [goal_spec] where goal_spec is one of the following:

    H1 .. Hn : generate a goal using hypotheses H1 .. Hn
   -H1 .. Hn : generate a goal using all hypotheses but H1 .. Hn
           # : generate a goal for the premise in which all hypotheses can be
               used. This is only allowed when specializing H : P -★ Q where
               either P or Q is persistent.
           % : generate a goal for a pure premise.

We may want to do the same for iIntros ? and iDestruct "H" as {?} "H",
but that requires more work. However, I do not think I want to rely on
names chosen this way.