see https://github.com/tonsky/FiraCode/wiki/VS-Code-Instructions

Fix a proof broken on Coq master

See merge request iris/iris!822

Add later credits to the WP

See merge request iris/iris!808

Make validy lemmas for `excl_auth` and `(u)frac_auth` more consistent with `auth`.

See merge request iris/iris!804

and `frac_auth_frag_valid_op_1_l`, add `frac_auth_frag_op_validN` and
`frac_auth_frag_op_valid`, which are bi-implications with arbitrary fractions.

Remove unused Qp argument to dfrac_valid_discarded

See merge request iris/iris!819

add mono_nat_lb_own_0

See merge request iris/iris!817

general lemma that a fixpoint is Persistent/Absorbing/Affine

See merge request iris/iris!810

Make saved props have discardable fractions

See merge request iris/iris!802

Tweak priority of proof mode instances for £.

Closes #470

See merge request iris/iris!818

- Rename `excl_auth_frag_validN_op_1_l` into `excl_auth_frag_op_validN` and
  `excl_auth_frag_valid_op_1_l` into `excl_auth_frag_op_valid` (similar to
  `auth_auth_op_valid`, and make them bi-implications.
- Add `excl_auth_auth_op_validN` and `excl_auth_auth_op_valid`

This closes issue #470.

Fupd soundness lemmas always generate credits

See merge request iris/iris!815

document wp_smart_apply

See merge request iris/iris!811

add proofmode instances for le_upd

See merge request iris/iris!813