Skip to content

Pull requests: rocq-prover/rocq

New pull request New
82 Open 10,596 Closed
82 Open 10,596 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 rely on canonical names in Coercionops table. kind: cleanup Code removal, deprecation, refactorings, etc.
#21192 opened Oct 11, 2025 by ppedrot Loading… 9.2+rc1
@SkySkimmer
Rely on user names for projection table in extraction. kind: cleanup Code removal, deprecation, refactorings, etc.
#21191 opened Oct 11, 2025 by ppedrot Loading… 9.2+rc1
Constant effects in Reductionops are now registered per user name. kind: cleanup Code removal, deprecation, refactorings, etc.
#21190 opened Oct 11, 2025 by ppedrot Loading… 9.2+rc1
Deprecate some set / map structures based on canonical names in Names. kind: cleanup Code removal, deprecation, refactorings, etc. needs: overlay This is breaking external developments we track in CI.
#21189 opened Oct 11, 2025 by ppedrot Loading… 9.2+rc1
@SkySkimmer
Add dev/ci/ci-env.sh which can be sourced to set paths for CI needs: squashing Some commits should be squashed together.
#21186 opened Oct 9, 2025 by SkySkimmer Loading…
@mattam82
3
Always set -e in ci-common needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#21185 opened Oct 9, 2025 by SkySkimmer • Draft
Merge the Dumpglob API to start dumping and to push a glob output. kind: cleanup Code removal, deprecation, refactorings, etc.
#21184 opened Oct 9, 2025 by ppedrot Loading… 9.2+rc1
@SkySkimmer
rm problematic variables under evars for evar instantiation
#21180 opened Oct 9, 2025 by Tragicus Loading…
6 tasks
35
Try βδι-reducing the type shape in w_unify_to_subterm. kind: experiment
#21179 opened Oct 9, 2025 by ppedrot • Draft
5
Ltac2 module inspection API kind: feature New user-facing feature request or implementation. needs: changelog entry This should be documented in doc/changelog. needs: test-suite update Test case should be added to / updated in the test-suite. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
#21178 opened Oct 8, 2025 by SkySkimmer • Draft 9.2+rc1
Print Assumptions store full globref instead of just label in Axiom kind: internal API, ML documentation...
#21175 opened Oct 7, 2025 by SkySkimmer Loading… 9.2+rc1
6
Deprecate Names.Label kind: internal API, ML documentation... needs: overlay This is breaking external developments we track in CI.
#21174 opened Oct 7, 2025 by SkySkimmer Loading… 9.2+rc1
1
@ppedrot
Doc: mention open_constr for ltac1 and update related doc kind: documentation Additions or improvement to documentation.
#21171 opened Oct 7, 2025 by SkySkimmer Loading… 9.2+rc1
1
Attribute to control scheme declaration kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: overlay This is breaking external developments we track in CI.
#21163 opened Oct 3, 2025 by SkySkimmer Loading… 9.2+rc1
1
8
WIP statically control access to summary needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#21160 opened Oct 3, 2025 by SkySkimmer • Draft
Refine the notation-incompatible-prefix warning kind: user messages Error messages, warnings, etc.
#21159 opened Oct 3, 2025 by proux01 • Draft
3 of 8 tasks
9.2+rc1
Properly handle Timeout x Fail cmd kind: fix This fixes a bug or incorrect documentation.
#21149 opened Oct 1, 2025 by SkySkimmer Loading…
1
Experiment: stricter associativity needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#21126 opened Sep 26, 2025 by ia0 • Draft
16
opam package use relocatable mode kind: infrastructure CI, build tools, development tools.
#21117 opened Sep 25, 2025 by SkySkimmer Loading… 9.2+rc1
2
Draft: Show diffs in Show, Show n and Show ident commands (for Proof General) kind: bug An error, flaw, fault or unintended behaviour. 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: diffs The diff mechanism for printing.
#21103 opened Sep 21, 2025 by jfehrle • Draft
1
1
Add a generic mechanism for rewriting with any equality satisfying J needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run.
#21098 opened Sep 19, 2025 by tabareau Loading…
154
Nix: cleanup, refactor, modernize needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#21093 opened Sep 18, 2025 by faukah • Draft
4
Equivalent-keys in ssrmatching needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#21084 opened Sep 12, 2025 by Tragicus • Draft
6 tasks
1
Typeclass resolution during unification needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run.
#21083 opened Sep 12, 2025 by Tragicus • Draft
6 tasks
1
[Corelib] Retrieve ring/field/micromega computational part from Stdlib 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: core library Corelib in theories/ part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.
#21080 opened Sep 11, 2025 by proux01 Loading…
2 of 5 tasks
9.2+rc1
7
ProTip! Add no:assignee to see everything that’s not assigned.