Notably this support relies on string to identifier conversion, which
works natively using Ltac2 in Coq 8.11+ and with a plugin
(https://github.com/ppedrot/coq-string-ident) in Coq 8.10. To use it,
you must replace intro_patterns.string_to_ident_hook with a real
implementation; see https://gitlab.mpi-sws.org/iris/string-ident for a
working implementation that works with Coq 8.11 (using Ltac2).

The syntax is %H (within a string intro pattern). This is technically
backwards-incompatible, because this was previously supported and parsed
as % and H separately. To restore the old behavior, separate with a
space, eg [% H].

Add insert delete lemma for big ops over gmap

See merge request iris/iris!420

add pair_included, auth_frag_core, singleton_core_total

See merge request iris/iris!421

Generalize `Excl_included` & more `singleton_included` lemmas

See merge request iris/iris!419

Rename existing asymmetric lemma `singleton_included` into `singleton_included_l`.

add OFE structure for Prop

See merge request iris/iris!418

Remove namespaces from lock API.

See merge request iris/iris!416

Better proof mode support for telescope + add missing BI instances

See merge request iris/iris!415

Also make better use of `Implicit Types` and group instances better.

Notion of composition on `oFunctor`s, and some renaming

See merge request iris/iris!411

`{o,r,ur}Functor_map_{ne,id,compose,contractive}`.

Make `_iff` and `_alter` lemmas for invariants consistent, and add `_iff` lemma for locks

See merge request iris/iris!414