GitLab

Update CHANGELOG for 1.3 release.

See merge request iris/stdpp!127

Fix both an error by my, and a provide compatibility with older Coq versions
whose `lia` is less powerful.

Make lemmas for `seq` and `seqZ` consistent.

Closes #57

See merge request iris/stdpp!126

Robbert/lookup total lemmas

Closes #50

See merge request iris/stdpp!125

For other operations, like `<$>`,  such lemmas appear to make little sense, since
they require premises involving `!!`.

Remove copyright headers, update LICENCE file.

Closes #54

See merge request iris/stdpp!124

This follows iris!387
This closes issue #54.

Change mode of `TCEq`.

See merge request iris/stdpp!123

Set `Hint Mode` for logical `TCX` type classes

Closes #55

See merge request iris/stdpp!121

Avoid using Hint Resolve with a term

See merge request iris/stdpp!122

This feature is now deprecated in Coq master (see
https://github.com/coq/coq/pull/7791).

Instead of passing a partially-applied lemma directly to Hint Resolve,
first create a definition and then make that reference a hint.

Rename `fin_of_nat` → `nat_to_fin` to follow the conventions.

See merge request iris/stdpp!120

Add destruct_or tactics to (possibly repeatedly) split disjunctions in an assumption

See merge request iris/stdpp!117

The opposite was true before to this commit.

Countable instance for vec, and rename `vec_to_list_of_list` into `vec_to_list_to_vec`

See merge request iris/stdpp!115