Skip to content

Pull requests: rocq-prover/rocq

New pull request New
84 Open 10,280 Closed
84 Open 10,280 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

RR CClosure it_mkLambda gives wrong environment size needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20729 opened Jun 8, 2025 by yannl35133 Loading…
2 tasks done
1
Update version number for 9.2+alpha needs: coq release Should not be merged until the next version has been branched (see milestone).
#20725 opened Jun 6, 2025 by SkySkimmer • Draft
Document an error with variants kind: documentation Additions or improvement to documentation.
#20723 opened Jun 6, 2025 by Villetaneuse Loading… 9.2+rc1
1
Tweak the native compilation scheme of cofixpoints. kind: cleanup Code removal, deprecation, refactorings, etc. kind: performance Improvements to performance and efficiency.
#20719 opened Jun 5, 2025 by ppedrot Loading… 9.1+rc1
5
Some stdlib -> corelib renaming
#20714 opened Jun 5, 2025 by proux01 Loading…
6 tasks
4
Fix #20679: avoid spurious newline in rocqdoc blocks. kind: documentation Additions or improvement to documentation. kind: infrastructure CI, build tools, development tools.
#20710 opened Jun 4, 2025 by Zimmi48 Loading… 9.0.1
1
3
Search for "rocq doc" instead of "coqdoc" in coqdoc/main.py kind: cleanup Code removal, deprecation, refactorings, etc.
#20709 opened Jun 4, 2025 by Villetaneuse Loading… 9.1+rc1
@SkySkimmer
13
ssr: skip impargs in pattern FO unif
#20707 opened Jun 3, 2025 by gares • Draft
1 of 6 tasks
14
[ci] Test composed Rocq build with Stdlib needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20705 opened Jun 3, 2025 by ejgallego • Draft
1
Add some code-blocks in sphinx README needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20700 opened Jun 3, 2025 by Villetaneuse • Draft
6 tasks
Remove bugged Loose Hint Behavior and fix incorrect Import optim
#20698 opened Jun 2, 2025 by SkySkimmer Loading… 9.1+rc1
nativecode don't generate forcecofix for non coinductive primproj kind: cleanup Code removal, deprecation, refactorings, etc. kind: performance Improvements to performance and efficiency.
#20696 opened Jun 2, 2025 by SkySkimmer Loading… 9.1+rc1
@ppedrot
3
Update opam version used in bench (2.1.3 -> 2.3.0) + cleanup script parts about job count kind: infrastructure CI, build tools, development tools.
#20687 opened May 28, 2025 by SkySkimmer Loading… 9.1+rc1
4
Option to internalize a qualid passed to an Ltac as a constr with its impargs kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: fixing The proposed code change is broken. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. part: ltac Issues and PRs related to the Ltac tactic language.
#20682 opened May 26, 2025 by SkySkimmer Loading…
22
Guard against parser modification in interp phase needs: independent fix The PR reveals an independent bug.
#20674 opened May 23, 2025 by SkySkimmer • Draft
7
Update plugin tuto kind: documentation Additions or improvement to documentation.
#20670 opened May 22, 2025 by SkySkimmer Loading… 9.1+rc1
Update parsing md & mention it in plugin tuto mlg files kind: documentation Additions or improvement to documentation.
#20669 opened May 22, 2025 by SkySkimmer Loading… 9.1+rc1
7
Reference not found error suggests similar names kind: user messages Error messages, warnings, etc.
#20662 opened May 20, 2025 by SkySkimmer • Draft
8
Search: allow typos when searching by string needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20660 opened May 20, 2025 by SkySkimmer • Draft
3
Ltac2 add $hyp:id quotation for dynamic hypotheses (where &id is static) kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
#20656 opened May 20, 2025 by SkySkimmer Loading… 9.1+rc1
@ppedrot
6
Fix wrong threading of cv_pb/pb in unification.ml needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20652 opened May 19, 2025 by mattam82 • Draft
6 tasks
3
More type enforced "instantiation" of constr patterns kind: cleanup Code removal, deprecation, refactorings, etc.
#20644 opened May 16, 2025 by SkySkimmer Loading… 9.1+rc1
Remove KerPair.SyntacticOrd kind: cleanup Code removal, deprecation, refactorings, etc. needs: discussion Further discussion is needed.
#20642 opened May 16, 2025 by SkySkimmer Loading…
@ppedrot
1
Share closures in the VM. kind: experiment 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.
#20634 opened May 14, 2025 by ppedrot Loading…
17
[tauto] change proof search strategy kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: performance Improvements to performance and efficiency. needs: benchmarking Performance testing is required. needs: fixing The proposed code change is broken. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run.
#20627 opened May 12, 2025 by fajb Loading…
19
ProTip! What’s not been updated in a month: updated:<2025-05-08.