Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
S
stdpp
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Monitor
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Iris
stdpp
Merge requests
Open
29
Merged
543
Closed
51
All
623
Actions
Subscribe to RSS feed
Toggle search history
Recent searches
You don't have any recent searches
Updated date
Priority
Created date
Updated date
Closed date
Milestone due date
Popularity
Label priority
Title
Folding Map
!597
·
created
1 month ago
by
Rudy Peterson
Closed
updated 1 week ago
add some sublist lemmas
!590
·
created
3 months ago
by
Kimaya Bedarkar
S-waiting-for-review
Closed
updated 1 week ago
Finite Map Helper Lemmas
!598
·
created
1 month ago
by
Rudy Peterson
Closed
updated 3 weeks ago
Draft: Add law `map_fold_foldr` to `FinMap` interface.
!565
·
created
9 months ago
by
Robbert Krebbers
Closed
updated 9 months ago
Prevent [finite_countable] from solving unrelated evars
1 of 4 checklist items completed
!424
·
created
2 years ago
by
Paolo G. Giarrusso
Closed
updated 10 months ago
Adapt to https://github.com/coq/coq/pull/18928
!549
·
created
1 year ago
by
Pierre Roux
Closed
updated 1 year ago
Draft: add lemma lookup_insert_eq
!507
·
created
1 year ago
by
Ralf Jung
Closed
updated 1 year ago
Use hint mode + more often
!435
·
created
2 years ago
by
Robbert Krebbers
S-waiting-for-author
Closed
updated 1 year ago
Replace `MGuard` with `MFail`
!488
·
created
1 year ago
by
Adam
Closed
updated 1 year ago
Add MRaise typeclass
!501
·
created
1 year ago
by
Thibaut Pérami
Closed
updated 1 year ago
add make_simple_intropattern
!515
·
created
1 year ago
by
Ralf Jung
Closed
updated 1 year ago
Add greater or equal symbol for numbers
!499
·
created
1 year ago
by
Thibaut Pérami
Closed
updated 1 year ago
make empty operational typeclass TC opaque
!474
·
created
2 years ago
by
Ralf Jung
Closed
updated 1 year ago
Enable `Hint Mode Equiv` now that stdpp requires Coq 8.12
!437
·
created
2 years ago
by
Paolo G. Giarrusso
Closed
updated 2 years ago
Add NoDup_bind, vec_enum, vec_finite.
!451
·
created
2 years ago
by
Herman Bergwerf
Closed
updated 2 years ago
Draft: dune build scripts
!387
·
created
2 years ago
by
Paolo G. Giarrusso
S-waiting-for-author
Closed
updated 2 years ago
lookup_gset_to_gmap: use decide rather than guard
!436
·
created
2 years ago
by
Ralf Jung
Closed
updated 2 years ago
Introduce `set_bind` and associated lemmas.
!383
·
created
3 years ago
by
Dan Frumin
Closed
1
updated 2 years ago
Add the feed revert, efeed revert, efeed inversion, and efeed destruct tactics
!389
·
created
2 years ago
by
Michael Sammler
Closed
updated 2 years ago
Add `set_map_2` and associated lemmas.
!381
·
created
3 years ago
by
Dan Frumin
Closed
updated 3 years ago
Previous
Next