Relax subG mode

See merge request iris/iris!255

More simple changes to make proof mode terms more compact.

See merge request iris/iris!253

With Coq master, we otherwise fail to infer instances with subG_savedAnythingΣ, which leads to goals like

> looking for (subG
>                       (@savedAnythingΣ (@ofe_funCF val (fun _ : val => laterCF idCF))
>                          ?cFunctorContractive0) Σ)

This is a follow up of !248.

Allow up to 10 introduction patterns for iInv.

See merge request iris/iris!252

Add renaming for `auth`  to CHANGELOG

See merge request iris/iris!251

Simple changes to make proof mode terms more compact

See merge request iris/iris!248

Joseph Tassarotti authored 5 years ago and Robbert Krebbers committed 5 years ago

Also fixes pre-existing bug in iCombine error messages.

More consistent naming for `auth`.

See merge request iris/iris!250

This MR is a follow up on the renamings performed (implicitly) as part of
!215. This MR makes the following changes:

- `auth_both_frac_valid` and `auth_both_valid` are now of the same shape
  as `auth_both_frac_validN` and `auth_both_validN`. That is, both are
  now biimplications.
- The left-to-right  direction of `auth_both_frac_valid` and
  `auth_both_valid` only holds in case the camera is discrete. The
  right-to-left versions for non-discrete cameras are prefixed `_2`, the
  convention that we use throughout the development.
- Change the direction of lemmas like `auth_frag_valid` and
  `auth_auth_valid` so that it's consistent with the other lemmas. I.e.
  make sure that the ◯ and ● are always on the LHS of the biimplication.

Make authoritative part of auth fractional

See merge request iris/iris!215

Make `iFresh` faster

See merge request iris/iris!247

Export that iPreProp is a Cofe

See merge request iris/iris!246

Generalize `iPureIntro` to support non-empty spatial contexts with just affine hypotheses.

See merge request !241

Never used `Declare Instance`.