Skip to content

Pull requests: rocq-prover/rocq

New pull request New
95 Open 10,379 Closed
95 Open 10,379 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Do not keep readding modules when computing self inclusions. kind: cleanup Code removal, deprecation, refactorings, etc.
#20866 opened Jul 3, 2025 by ppedrot Loading… 9.2+rc1
Do not pass the "core" database twice in hint tactics. kind: fix This fixes a bug or incorrect documentation.
#20865 opened Jul 3, 2025 by ppedrot Loading… 9.1.0
1
2
Do not redeclare functor parameters in Declaremods. kind: cleanup Code removal, deprecation, refactorings, etc.
#20863 opened Jul 3, 2025 by ppedrot Loading… 9.2+rc1
@SkySkimmer
Backports 9.1
#20860 opened Jul 3, 2025 by gares Loading… 9.1+rc1
@SkySkimmer
8
Fix type-classes article and add doi for citation. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20859 opened Jul 2, 2025 by ErrWare Loading…
1
WIP release summary kind: documentation Additions or improvement to documentation. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20856 opened Jul 2, 2025 by SkySkimmer • Draft 9.1.0
1
Replace keyword "Notation" by "Abbreviation" for abbreviations kind: deprecation Deprecation part: notations The notation system.
#20855 opened Jul 2, 2025 by proux01 Loading…
3 of 6 tasks
9.2+rc1
7
Remove Mltop.module_is_known, now fully handled by Findlib kind: cleanup Code removal, deprecation, refactorings, etc. needs: overlay This is breaking external developments we track in CI.
#20853 opened Jul 2, 2025 by SkySkimmer Loading… 9.2+rc1
@ppedrot
2
Support for enabling and disabling string and number notations. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20848 opened Jul 1, 2025 by gmalecha Loading…
6 tasks
1
Congruence: naive support for primitive arrays needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20840 opened Jul 1, 2025 by Janno • Draft
8 tasks
Ubuntu 20.04 is EOL (move base to 22.04) kind: infrastructure CI, build tools, development tools. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. part: CI The continuous integration system.
#20838 opened Jun 30, 2025 by andres-erbsen Loading… 9.2+rc1
22
Ltac2 type ltac_constant <> KerName.t kind: cleanup Code removal, deprecation, refactorings, etc. needs: fixing The proposed code change is broken.
#20837 opened Jun 30, 2025 by SkySkimmer Loading… 9.2+rc1
2
Ltac2: Add a basic ability to declare definitions using ltac2 tactics needs: discussion Further discussion is needed. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20828 opened Jun 30, 2025 by KacperFKorban Loading…
1 of 6 tasks
1
Retain original variable names for patterns in Print HintDb kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. part: hints Hint mechanism, databases, etc.
#20827 opened Jun 30, 2025 by jfehrle Loading…
3 tasks
9.2+rc1
15
Set firstorder solver explicitly to auto with core in prelude kind: cleanup Code removal, deprecation, refactorings, etc. needs: independent fix The PR reveals an independent bug.
#20820 opened Jun 27, 2025 by TheoWinterhalter Loading… 9.2+rc1
@ppedrot
8
Native compute use OCaml Lazy.t instead of adhoc ref kind: cleanup Code removal, deprecation, refactorings, etc.
#20817 opened Jun 26, 2025 by SkySkimmer Loading… 9.2+rc1
@ppedrot
10
Abbreviations don't add printing rule when still qualified kind: fix This fixes a bug or incorrect documentation. kind: user messages Error messages, warnings, etc. needs: progress Work in progress: awaiting action from the author. part: notations The notation system.
#20816 opened Jun 26, 2025 by SkySkimmer Loading… 9.2+rc1
1
@proux01
6
Implement Extensible Attributes on Definitions needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20812 opened Jun 25, 2025 by gmalecha Loading…
4 tasks
8
Automatically generated goal names kind: feature New user-facing feature request or implementation.
#20809 opened Jun 25, 2025 by dhalilov • Draft
4 of 5 tasks
41
ci-cross-crypto keep build_ci for the minimizer kind: infrastructure CI, build tools, development tools.
#20801 opened Jun 25, 2025 by SkySkimmer Loading… 9.2+rc1
5
Enable eta in TC unification needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20798 opened Jun 24, 2025 by Janno • Draft
6 tasks
Ltac2: Add revgoals needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20796 opened Jun 24, 2025 by KacperFKorban Loading…
2 tasks done
9.2+rc1
1
@SkySkimmer
5
Backtrack on eta in tactic unification
#20795 opened Jun 24, 2025 by Janno • Draft
6 tasks
19
Add equal for reference in Ltac2 needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20794 opened Jun 24, 2025 by Villetaneuse Loading…
1 task done
@ppedrot
3
Proof of concept: typeclass resolution using a default state with all definitions opaque. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20786 opened Jun 20, 2025 by mattam82 • Draft
17
ProTip! Type g i on any issue or pull request to go back to the issue listing page.