Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Draft: Avoid making definitions from stdlib type class transparent

!641 created by Robbert Krebbers
Add `Hint Mode` for `Equivalence`.

!640 created by Robbert Krebbers
Add build flag `deprecated-reference-since-9.1`.

!639 created by Robbert Krebbers
Remove old workarounds for deprecated results in Rocq.

!638 created by Robbert Krebbers
Remove dependency on soon to be deprecated `Znumtheory`.

!637 created by Robbert Krebbers
S-blocked
Use Rocq 9.0 for test output.

!636 created by Robbert Krebbers
Forgotten changes in MR 632.

!635 created by Rodolphe Lepigre
Trigger dune CI in MRs with [CI-dune-job] label.

!634 created by Rodolphe Lepigre
CI-dune-job
rename opam packages to rocq-*

!633 created by Ralf Jung
gen_CoqProject: rename 'local-flags' to 'local' since it is different from 'flags'

!632 created by Ralf Jung
try dune job with Rocq 9.1.dev

!631 created by Ralf Jung
Add test for universes, still commented since it needs Rocq 9.0.

!630 created by Robbert Krebbers
Provide support for `is_Some None` in the tactics `done` and `naive_solver`.

!629 created by Robbert Krebbers
fin_maps: generalise map currying/uncurrying

!628 created by Isaac van Bakel
Comment the file coPset.v.

!627 created by François Pottier
Avoid potential loops related to `compose`.

!626 created by Janno
S-waiting-for-author
Disable the dune build in CI.

!625 created by Rodolphe Lepigre
Add lemma const_fmap_strong

!624 created by Kimaya Bedarkar
sublist lemmas

!623 created by Kimaya Bedarkar
Add some missing map and set lemmas

!622 created by Johannes Hostert