Skip to content

Pull requests: rocq-prover/rocq

New pull request New
95 Open 10,384 Closed
95 Open 10,384 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

rocq doc replace @@TITLE@@ in header with page title, use in corelib
#20907 opened Jul 11, 2025 by SkySkimmer Loading…
1
Use option type in rocqdoc arg handling for header/footer kind: cleanup Code removal, deprecation, refactorings, etc.
#20906 opened Jul 11, 2025 by SkySkimmer Loading…
Fix link in corelib doc header needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20905 opened Jul 11, 2025 by SkySkimmer Loading…
Remove argument duplication in intern_tacarg kind: cleanup Code removal, deprecation, refactorings, etc.
#20904 opened Jul 11, 2025 by SkySkimmer Loading…
Ignore module redeclaration in Print Module commands. kind: cleanup Code removal, deprecation, refactorings, etc.
#20903 opened Jul 11, 2025 by ppedrot Loading… 9.2+rc1
@SkySkimmer
1
Cleanups around induction scheme lookups kind: cleanup Code removal, deprecation, refactorings, etc.
#20902 opened Jul 11, 2025 by SkySkimmer Loading… 9.2+rc1
@ppedrot
6
Add test for #17188 kind: infrastructure CI, build tools, development tools.
#20896 opened Jul 10, 2025 by SkySkimmer Loading… 9.2+rc1
1
Deprecate "Proof term" command kind: user messages Error messages, warnings, etc.
#20893 opened Jul 10, 2025 by SkySkimmer Loading… 9.2+rc1
1
Cleanup pretyping API needs: fixing The proposed code change is broken. needs: merge of dependency This PR depends on another PR being merged first. needs: overlay This is breaking external developments we track in CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run.
#20892 opened Jul 10, 2025 by SkySkimmer Loading… 9.2+rc1
@ppedrot
Fix synterp/interp phase splitting in plugins initializations kind: fix This fixes a bug or incorrect documentation.
#20888 opened Jul 10, 2025 by SkySkimmer Loading… 9.2+rc1
@ppedrot
2
Assert that modules are not redeclared in Environ API. kind: cleanup Code removal, deprecation, refactorings, etc. needs: merge of dependency This PR depends on another PR being merged first.
#20885 opened Jul 8, 2025 by ppedrot Loading… 9.2+rc1
11
rocq dep: register files in ROCQPATH for extra deps needs: fixing The proposed code change is broken.
#20878 opened Jul 8, 2025 by SkySkimmer Loading…
1
2
Make "unable to handle arbitrary u+k <= v constraints" a regular error kind: fix This fixes a bug or incorrect documentation.
#20876 opened Jul 8, 2025 by SkySkimmer Loading… 9.1.0
4
@ppedrot
3
Capture Output control and Test Output command for asserting outputs of vernac commands. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20873 opened Jul 7, 2025 by radrow • Draft
2
[parsing] Warn about another recovery mechanism kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: parser The parser (also called gramlib, forked from camlp5)
#20870 opened Jul 6, 2025 by proux01 Loading… 9.2+rc1
@ppedrot
4
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
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
10
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
3
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…
1 task done
9.2+rc1
28
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 kind: internal API, ML documentation... needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. needs: progress Work in progress: awaiting action from the author.
#20812 opened Jun 25, 2025 by gmalecha Loading…
1 of 3 tasks
9.2+rc1
@SkySkimmer
26
ProTip! Type g i on any issue or pull request to go back to the issue listing page.