The idea is to avoid unnecessary calls to iRename: when choosing names
for sub-patterns, instead of generating fresh names or reusing an
existing (unrelated) name, if the sub-pattern is an identifier, then
directly chose this identifier as the new name, thus saving a rename
later on.

[triviality] Clarify funny proof of `tac_twp_cmpxchg_fail`

See merge request iris/iris!738

To avoid confusion from
iris/iris@d2c226e7 (comment 73999).

add big_sepL_take_drop

See merge request iris/iris!734

add big_sep*_sep_2 lemmas for merging bigops via iDestruct

See merge request iris/iris!736

Optimize iIntoEmpValid

See merge request iris/iris!729

With large proof contexts and lemmas with many forall quantifiers,
iIntoEmpValid can become quite slow. This makes it go faster by adding
"fast paths" for the -> and forall cases, gated by Ltac pattern
matching (which is faster than trying to unify with refine and fail).

Fix and improve `iSpecialize` auto framing error message.

Closes #432

See merge request iris/iris!730

make binary wand/view shift connectives 'block' formated

See merge request iris/iris!727

This closes issue #432.

na_invariants: deduplicate proof of fresh_inv_name

See merge request iris/iris!728

Debatable, but the proof context of `na_inv_alloc` writes `ε` instead of `CoPSet
∅`.

Add generalized implication lemma for big_sepM

See merge request iris/iris!697

suggested by Huge Herbelin

Printing improvements

See merge request iris/iris!726