Iris 3.5.0 release notes

Closes #435

See merge request !748

Improve documentation of convention for `AsFractional` instances

See merge request !747

update package descriptions

Closes #436

See merge request !746

Prove missing fractional_big_sepL2

See merge request !737

To match the suggestion in
!737 (comment 75017).

fixes #437

Editor docs: add information on how to use vim for working with Iris

See merge request !744

Normalize focused goal output

See merge request !743

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

relax AsFractional Hint Mode

See merge request !740

Optimize iDestruct by avoiding superfluous iRenames

See merge request !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 !738

To avoid confusion from
d2c226e7 (comment 73999).

add big_sepL_take_drop

See merge request !734

add big_sep*_sep_2 lemmas for merging bigops via iDestruct

See merge request !736