alternative overlay for coq/coq#12162

See merge request iris/stdpp!159

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

See merge request iris/stdpp!157

Add Countable instance for Ascii.ascii

See merge request iris/stdpp!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 iris/stdpp!141

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

See merge request iris/stdpp!145

Another try at removing strings.length

See merge request iris/stdpp!144

Add tests for equiv notation

See merge request iris/stdpp!143

Extracted from iris!409.

Add notation `wn` of weakly normalizing terms; and prove some common theorems about it.

See merge request !140

Revise uses of inj as discussed

See merge request !138