use new select tactic from std++

See merge request iris/iris!438

Make core_id_local_update work with fractional authority

See merge request !430

CHANGELOG.md: Fix typo

See merge request !437

Add mapsto_ne helper lemma

See merge request !417

Here's one case this lemma might be useful. Suppose we want to
programmatically generate namespaces for e.g. locks:

```
Definition lockN (l : loc) := nroot .@ "lock" .@ l.
```

Then to know that two such namespaces are disjoint, we need to know
that the corresponding locations are distinct. For that we use
the lemma here introduced.

```
Lemma ne l1 l2 v1 v2 :
  l1 ↦ v1 -∗ l2 ↦ v2 -∗ ⌜l1 ≠ l2⌝.
Proof. iApply mapsto_mapsto_ne. (* goal ¬ ✓ 2%Qp *) by intros []. Qed.
```

Improve `coreP` construction.

See merge request !436

Rename auth_both_frac_op into auth_both_op

See merge request !434

Simon Friis Vindum authored 4 years ago and Ralf Jung committed 4 years ago

Removes auth_both_op and renames auth_both_frac_op into auth_both_op.

Fix some typos in docs

See merge request !433

Add heap_lang lib for "invariant locations": locations with a (pure) invariant attached to them

See merge request !289

Make use of `▷^` notation in its definition.

See merge request !428

Fix notation issues in #302 and add some missing "operator sections" for (bi)entailment

Closes #302

See merge request !409

This works because there is already a `Reserved Notation`.

Fixed a spacing issue in metatheory.v

See merge request !427

Fix #302, including their ASCII variants.
- Don't use quotes `'` that are not surrounded by spaces.
- However, notation `'(⊢@{' PROP } )` prevents parsing `(⊢@{PROP} Q)` using the
`⊢@{PROP} Q` notation.

To fix that, we force left-factorization: we add a notation for `'(⊢@{' PROP }
Q )`, defined to coincide with '⊢@{' PROP } Q but which can be left-factored
with `( '⊢@{' PROP } )`.

- Add left and right operator sections for (bi)entailment
- Add tests.

Also do all of the above also for ASCII notations, except for operator sections,
which seem to require more discussion.