Skip to content

Pull requests: coq/coq

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

Pull requests list

Add Ltac2.String.sub. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
#19204 opened Jun 12, 2024 by rlepigre Loading…
hcons: remove land 0x3FFFFFFF needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19202 opened Jun 12, 2024 by SkySkimmer Loading…
8
Fix incorrectly flipped implementation of Cumulativity Weak Constraints kind: fix This fixes a bug or incorrect documentation.
#19201 opened Jun 12, 2024 by SkySkimmer Loading… 8.20+rc1
Cleanup vernac_classifier results needs: fixing The proposed code change is broken.
#19199 opened Jun 11, 2024 by SkySkimmer Loading…
13
Add detailed instructions to update the Zenodo record. kind: documentation Additions or improvement to documentation. kind: meta About the process of developing Coq.
#19198 opened Jun 10, 2024 by Zimmi48 Loading…
1
Ltac2: add a few APIs about uint63 kind: feature New user-facing feature request or implementation. needs: changelog entry This should be documented in doc/changelog. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19197 opened Jun 10, 2024 by SkySkimmer Loading…
Don't refresh universes when pretyping cast kind: fix This fixes a bug or incorrect documentation.
#19196 opened Jun 10, 2024 by SkySkimmer Loading… 8.20+rc1
1
@ppedrot
4
[vernacstate] Remove Vernacstate.Parser.t kind: cleanup Code removal, deprecation, refactorings, etc. part: vernac High level command interpretation.
#19193 opened Jun 9, 2024 by ejgallego Loading…
@SkySkimmer
17
Slightly tweak the bench diff colours. kind: infrastructure CI, build tools, development tools. needs: test-suite update Test case should be added to / updated in the test-suite.
#19190 opened Jun 9, 2024 by ppedrot Loading… 8.20+rc1
@SkySkimmer
Include warnings in the Errors panel 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: CoqIDE Issues and PRs related to CoqIDE or other IDE features of coq.
#19188 opened Jun 8, 2024 by jfehrle Loading…
1 task done
8.20+rc1
Removing indirection from global_declaration to constant_entry kind: cleanup Code removal, deprecation, refactorings, etc. needs: overlay This is breaking external developments we track in CI.
#19185 opened Jun 8, 2024 by herbelin Loading…
@SkySkimmer
7
Export side effects of transparent obligations 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. needs: progress Work in progress: awaiting action from the author. part: program
#19184 opened Jun 8, 2024 by herbelin Loading…
1 task done
8.21+rc1
3
[core] Improved state protection against memprof-limits interruptions 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.
#19177 opened Jun 7, 2024 by ejgallego • Draft 8.20+rc1
3
[lib] Add primitives for async-safe resource masking and thread_maps from memprof-limits kind: compatibility Changes allowing for compatibility between versions. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: internal API, ML documentation... part: ocaml
#19175 opened Jun 7, 2024 by ejgallego Loading…
15
Include constr hcons calls in profiling kind: internal API, ML documentation...
#19170 opened Jun 7, 2024 by SkySkimmer Loading…
2
CoqIDE: Make tabs reorderable and fix preference on tabs position needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19166 opened Jun 6, 2024 by Frigory33 Loading…
1 task done
Update/format CoqIDE FAQ file and update browser commands needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19165 opened Jun 6, 2024 by Frigory33 Loading…
39
Stop repairing bad relevances in the kernel kind: cleanup Code removal, deprecation, refactorings, etc.
#19164 opened Jun 6, 2024 by SkySkimmer Loading… 8.21+rc1
@ppedrot
12
Parse Type@{ Prop/SProp/Set | ... } rather than failing needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19163 opened Jun 6, 2024 by kyoDralliam Loading…
5 tasks
1
2
Experiment to avoid retypechecking repeated subterms in typeops needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19160 opened Jun 6, 2024 by SkySkimmer • Draft
28
Show tooltips for syntax errors kind: bug An error, flaw, fault or unintended behaviour. part: CoqIDE Issues and PRs related to CoqIDE or other IDE features of coq.
#19153 opened Jun 5, 2024 by jfehrle Loading…
1 of 2 tasks
8.20+rc1
1
8
Factoring and hiding evar-sensitive has_evar and head_evar kind: cleanup Code removal, deprecation, refactorings, etc.
#19151 opened Jun 5, 2024 by herbelin Loading… 8.21+rc1
@ppedrot
7
[notation] Change default levels for easier factorization of prefixes kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: notations The notation system. part: vernac High level command interpretation.
#19149 opened Jun 5, 2024 by proux01 Loading…
4 of 6 tasks
8.20+rc1
20
warnings or errors with a known fix needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19147 opened Jun 5, 2024 by gares • Draft
1 task
8.20+rc1
12
Simplify Proofview.run_tactic kind: cleanup Code removal, deprecation, refactorings, etc.
#19145 opened Jun 4, 2024 by SkySkimmer Loading…
ProTip! Updated in the last three days: updated:>2024-06-09.