Merge requests · Iris / stdpp · GitLab

Adapt to https://github.com/coq/coq/pull/18224

!536 · created Jan 09, 2024 by Pierre Roux
- Merged
- 21
updated Feb 02, 2024
Remove Import NPeano

!535 · created Nov 15, 2023 by Pierre Rousselin
- Merged
- 8
updated Nov 17, 2023
Make `inv` and `oinv` work with numbers

!534 · created Oct 27, 2023 by Ralf Jung
- Merged
- 10
updated Oct 30, 2023
Allow pattern and type annotations in propset notation

!533 · created Oct 18, 2023 by Thibaut Pérami
- Merged
- 35
updated Sep 11, 2024
Draft: Staging MR for various refactorings 2 of 5 checklist items completed

!532 · created Oct 16, 2023 by Robbert Krebbers
- 1
updated Dec 02, 2023
Fix inconsistencies in `lookup` and `elem_of` lemmas for `list`

!531 · created Oct 14, 2023 by Robbert Krebbers ci/refactor_staging
- Merged
- 21
updated Oct 20, 2023
Add lemma `lookup_total_fmap`.

!530 · created Oct 14, 2023 by Robbert Krebbers
- 9
updated Oct 16, 2023
Add `prod_swap` and some basic results for it.

!529 · created Oct 14, 2023 by Robbert Krebbers
- Merged
- 3
updated Oct 14, 2023
Missing `Params` instances for `prod_map` and `prod_zip`.

!528 · created Oct 14, 2023 by Robbert Krebbers
- Merged
updated Oct 14, 2023
Add a comment about `cancel_inj` and `cancel_surj`.

!527 · created Oct 14, 2023 by Robbert Krebbers
- 7
updated Oct 14, 2023
Provide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a single statement.

!526 · created Oct 14, 2023 by Robbert Krebbers ci/refactor_staging
- Merged
- 37
updated Oct 17, 2023
add inv and oinv tactics that are basically a smarter and fixed inversion_clear

!525 · created Oct 14, 2023 by Ralf Jung
- Merged
- 15
updated Oct 14, 2023
remove 'wf' alias for the standard 'well_founded'

!524 · created Oct 14, 2023 by Ralf Jung
- Merged
- 7
updated Oct 14, 2023
Improve comment of `TCEq`.

!523 · created Oct 06, 2023 by Robbert Krebbers
- Merged
- 3
updated Oct 07, 2023
Add `MThrow` and replace `MGuard`

!522 · created Oct 06, 2023 by Thibaut Pérami
- Merged
- 35
updated Oct 13, 2023
Add `TCSimpl` type class.

!521 · created Oct 06, 2023 by Robbert Krebbers
- Merged
- 12
updated Oct 13, 2023
Add instance `cons_equiv_inj`.

!520 · created Oct 06, 2023 by Robbert Krebbers
- Merged
updated Oct 06, 2023
Add lemmas for easy measure/size induction.

!519 · created Oct 06, 2023 by Robbert Krebbers
- Merged
- 31
updated Oct 14, 2023
Rework lemmas for `take/drop` of an `++`:

!518 · created Oct 05, 2023 by Robbert Krebbers
- Merged
- 3
updated Oct 05, 2023
Add lemmas for `reverse` of `take`/`drop`.

!517 · created Oct 05, 2023 by Robbert Krebbers
- Merged
- 2
updated Oct 05, 2023

Prev
1
2
3
4
5
6
7
…
29
Next