Merge requests · Iris / stdpp · GitLab

Allow compiling the packages with dune.

!552 · created May 18, 2024 by Rodolphe Lepigre
- Merged
- 49
updated Jun 17, 2024
Strengthen `map_disjoint_difference_{l,r}` and make them consistent with the lemmas for sets.

!551 · created May 02, 2024 by Robbert Krebbers
- Merged
updated Aug 14, 2024
Explicitly Require Coq Vector in vector.v (for coq/coq#18936)

!550 · created Apr 17, 2024 by Andres Erbsen
- Merged
- 9
updated Apr 19, 2024
prepare changelog for release

!548 · created Apr 12, 2024 by Ralf Jung
- Merged
- 1
updated Apr 12, 2024
always add Proof. after Restart.

!547 · created Apr 03, 2024 by Ralf Jung
- Merged
- 3
updated Apr 03, 2024
Add `inv select` and `inversion select` tactics

!546 · created Apr 03, 2024 by Ralf Jung
- Merged
- 1
updated Apr 03, 2024
Generalization of map_fold_comm_acc

!545 · created Apr 03, 2024 by Yannick Zakowski
- Merged
- 5
updated Apr 12, 2024
readme: mention more operations we block

!544 · created Apr 03, 2024 by Ralf Jung
- Merged
- 1
updated Apr 12, 2024
Cleanup bitblast_mod after dropping support for Coq 8.13

!543 · created Mar 12, 2024 by Michael Sammler
- Merged
updated Mar 12, 2024
create new package for stdpp-bitvector library

!542 · created Mar 11, 2024 by Ralf Jung
- Merged
- 45
updated Apr 15, 2024
Fix slowdown in bv_saturate from https://github.com/coq/coq/pull/17984

!541 · created Mar 11, 2024 by Michael Sammler
- Merged
- 2
updated Mar 11, 2024
Add lemma `join_app`.

!540 · created Feb 29, 2024 by Robbert Krebbers
- Merged
updated Mar 05, 2024
drop support for Coq 8.16 and 8.17

!539 · created Feb 05, 2024 by Ralf Jung
- Merged
- 2
updated Feb 07, 2024
test on Coq 8.19

!538 · created Feb 02, 2024 by Ralf Jung
- Merged
updated Feb 02, 2024
Adapt to https://github.com/coq/coq/pull/18590

!537 · created Jan 31, 2024 by Pierre Roux
- Merged
- 16
updated Feb 09, 2024
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
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

Prev
1
2
3
4
5
6
…
26
Next