Merge the "1 focused goal" line with the subsequent "(shelved: 1)" line,
since this is the new output in Coq 8.15+.

Iris does not currently produce this output, since no test calls `Show`
with shelved goals, but this future-proofs the test normalization.

make f_contractive consistent with f_equiv

See merge request iris/iris!741

relax AsFractional Hint Mode

See merge request !740

Optimize iDestruct by avoiding superfluous iRenames

See merge request iris/iris!733

Following up on the previous commit, this slightly generalizes the
lemmas associated to the intuitionistic/spatial/modalelim cases of
iDestruct to support renaming on the fly, and use these to save a
later renaming.

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 !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.