This gives a 25% speedup on some files (e.g. boxes).

This commit contains some hacks to work arround Coq issue #5699.

This commit requires Coq v8.7 together with

  https://github.com/coq/coq/pull/1006

(□ P) now means (bi_bare (bi_persistently P)).

This is motivated by the fact that these two modalities are rarely
used separately.

In the case of an affine BI, we keep the □ notation. This means that a
bi_bare is inserted each time we use □. Hence, a few adaptations need
to be done in the proof mode class instances.

The absence of this axiom has two consequences:

- We no longer have `■ (P ∗ Q) ⊢ ■ P ∗ ■ Q` and `□ (P ∗ Q) ⊢ □ P ∗ □ Q`,
  and as a result, separating conjunctions in the unrestricted/persistent
  context cannot be eliminated.
- When having `(P -∗ ⬕ Q) ∗ P`, we do not get `⬕ Q ∗ P`. In the proof
  mode this means when having:

    H1 : P -∗ ⬕ Q
    H2 : P

  We cannot say `iDestruct ("H1" with "H2") as "#H1"` and keep `H2`.

However, there is now a type class `PositiveBI PROP`, and when there is an
instance of this type class, one gets the above reasoning principle back.

TODO: Can we describe positivity of individual propositions instead of the
whole BI? That way, we would get the above reasoning principles even when
the BI is not positive, but the propositions involved are.

As Aleš observed, in the ordered RA model it is not, unless the order on the
unit is timeless.

Thanks to discussions with Ales and Amin.

Rename `UCMRA` → `Ucmra`
Rename `CMRA` → `Cmra`
Rename `OFE` → `Ofe` (`Ofe` was already used partially, but many occurences were missing)
Rename `STS` → `Sts`
Rename `DRA` → `Dra`

Now, we never need to unfold LimitPreserving in LambdaRust, and hence
the entails_lim tactic is no longer needed.

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

This fixes the following issue by JH Jourdan:

  The fact of including uPred_[...] in the module uPred (in base_logic.v),
  implies that typeclasses instances are declared twice. Once in module
  uPred and once in module uPred_[...]. This has the unfortunate
  consequence that it has to backtrack to both instances each time the
  first one fails, making failure of type class search for e.g.
  PersistentP potentially exponential.

  Goal ((□ ∀ (x1 x2 x3 x4 x5: nat), True -∗ True) -∗ True : iProp Σ).
    Time iIntros "#H".
    Undo.
    Remove Hints uPred_derived.forall_persistent : typeclass_instances.
    Time iIntros "#H".

Thanks to Jason Gross @ Coq club for suggesting this fix.

Using this new definition we can express being contractive using a
Proper. This has the following advantages:

- It makes it easier to state that a function with multiple arguments
  is contractive (in all or some arguments).
- A solve_contractive tactic can be implemented by extending the
  solve_proper tactic.

Use COFEs only for the recursive domain equation solver