Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Trigger dune CI in MRs with [CI-dune-job] label.

!634 created by Rodolphe Lepigre
CI-dune-job
Added some lemmas about [sublist]

!357 created by Jonas Kastberg
Use Rocq 9.0 for test output.

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

!639 created by Robbert Krebbers
rename opam packages to rocq-*

!633 created by Ralf Jung
Remove old workarounds for deprecated results in Rocq.

!638 created by Robbert Krebbers
Generate the [_CoqProject] file.

!604 created by Rodolphe Lepigre
Forgotten changes in MR 632.

!635 created by Rodolphe Lepigre
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 lemma const_fmap_strong

!624 created by Kimaya Bedarkar
fin map alter lemmas

!610 created by Rudy Peterson
Provide support for `is_Some None` in the tactics `done` and `naive_solver`.

!629 created by Robbert Krebbers
Add test for universes, still commented since it needs Rocq 9.0.

!630 created by Robbert Krebbers
Zip Theorems

!596 created by Rudy Peterson
Forall exists Forall2 lemmas

!620 created by Rudy Peterson
Add some missing map and set lemmas

!622 created by Johannes Hostert
Provide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a single statement.

!526 created by Robbert Krebbers ci/refactor_staging
Provide "lookup" and commuting lemmas as equations that always apply, and fix some inconsistent lemma naming 2 of 4 checklist items completed

!532 created by Robbert Krebbers
Fix inconsistencies in `lookup` and `elem_of` lemmas for `list`

!531 created by Robbert Krebbers ci/refactor_staging