Rotate everything

See merge request iris/stdpp!136

add map_Forall_lookup

See merge request !158

alternative overlay for coq/coq#12162

See merge request !159

tactics.v: Fix parsing precedence for `select` tactic

See merge request !157

Add Countable instance for Ascii.ascii

See merge request !154

fix imap_seq and imap_seq0 to make them useful

See merge request iris/stdpp!151

Create HintDBs with the discriminated option

See merge request iris/stdpp!148

Added select and select_revert tactics

See merge request iris/stdpp!142

According to the documentation
https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:cmd.create-hintdb,
when creating a hint database without discrimination, Coq uses the
legacy implementation, which only uses Discrimination Trees for goals
without evars and does not use opaqueness information. This commit
switches the hint databases of stdpp to the new implementation.

Add filter_app lemma

See merge request !147

Add `ProofIrrel ()`

See merge request iris/stdpp!146

This instance might seem odd, but `ProofIrrel` takes a `Type` and not a `Prop`,
and stdpp already has instances for products.

Extracted list_numbers.v with seq, seqZ, sum_list and max_list

See merge request !141

Add `encode_Z` function to encode element of countable type as `Z`.

See merge request !145

Another try at removing strings.length

See merge request !144

Add tests for equiv notation

See merge request !143

Extracted from iris!409.