8000 Pull requests · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Pull requests: rocq-prover/rocq

New pull request New
89 Open 10,261 Closed
89 Open 10,261 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

ssr: skip impargs in pattern FO unif
#20707 opened Jun 3, 2025 by gares • Draft
1 of 6 tasks
3
Post #20650 fixes needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#20706 opened Jun 3, 2025 by SkySkimmer Loading…
1
[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
Stop using "dummy_value" in native compute kind: cleanup Code removal, deprecation, refactorings, etc.
#20704 opened Jun 3, 2025 by SkySkimmer Loading… 9.1+rc1
@ppedrot
2
Genlambda names are not annotated with relevance kind: cleanup Code removal, deprecation, refactorings, etc.
#20702 opened Jun 3, 2025 by SkySkimmer Loading…
3
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
Native compute reduce mutability of accus
#20699 opened Jun 2, 2025 by SkySkimmer Loading…
@ppedrot
7
Remove bugged Loose Hint Behavior and fix incorrect Import optim
#20698 opened Jun 2, 2025 by SkySkimmer Loading…
nativecode don't generate forcecofix for non coinductive primproj needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run.
#20696 opened Jun 2, 2025 by SkySkimmer Loading… 9.1+rc1
@ppedrot
1
Provide names for exns with quotes in doc kind: documentation Additions or improvement to documentation.
#20694 opened May 30, 2025 by Villetaneuse Loading…
1
Remove the hypnaming API from Evarutil. kind: cleanup Code removal, deprecation, refactorings, etc.
#20689 opened May 28, 2025 by ppedrot Loading… 9.1+rc1
@SkySkimmer
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… 9.1+rc1
20
Change introduction to Ltac2 refman page kind: documentation Additions or improvement to documentation.
#20681 opened May 26, 2025 by Villetaneuse Loading… 9.0.1
1
Add anchors in Corelib html index kind: documentation Additions or improvement to documentation.
#20680 opened May 26, 2025 by Villetaneuse Loading… 9.0.1
@SkySkimmer
13
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
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… 9.1+rc1
16
ProTip! Add no:assignee to see everything that’s not assigned.
0