Skip to content

Pull requests: coq/coq

New pull request New
92 Open 9,505 Closed
92 Open 9,505 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Rocqify plugins kind: internal API, ML documentation...
#19698 opened Oct 16, 2024 by ppedrot Loading… 9.0 rc1
Genarg cleanups kind: cleanup Code removal, deprecation, refactorings, etc. kind: fix This fixes a bug or incorrect documentation.
#19697 opened Oct 16, 2024 by SkySkimmer Loading…
@ppedrot
1
Correct description of multiple hintdb handling 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.
#19696 opened Oct 15, 2024 by jfehrle Loading…
Fix unicode classification of non-spacing marks. kind: fix This fixes a bug or incorrect documentation. 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. part: parser The parser (also called gramlib, forked from camlp5)
#19693 opened Oct 15, 2024 by silene Loading… 9.0 rc1
1
Obligations, Proof, Hint Extern, tactic option commands do not depend on ltac1 kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: changelog entry This should be documented in doc/changelog. needs: documentation Documentation was not added or updated.
#19690 opened Oct 14, 2024 by SkySkimmer Loading… 9.0 rc1
2
Move ltac2-in-ltac1 genargs out of the core ltac2 plugin fix printers kind: cleanup Code removal, deprecation, refactorings, etc. kind: fix This fixes a bug or incorrect documentation.
#19687 opened Oct 14, 2024 by SkySkimmer Loading…
@ppedrot
5
Give Stdlib its own repository needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. needs: merge of dependency This PR depends on another PR being merged first.
#19686 opened Oct 14, 2024 by proux01 Loading…
5 of 8 tasks
8.20 backports
#19684 opened Oct 14, 2024 by proux01 • Draft
Refresh template levels in clenvs. kind: redesign The same functionality is being re-implemented in a different way.
#19680 opened Oct 12, 2024 by ppedrot • Draft
21
Remove syntax : typ in Obligation command (it was ignored) kind: cleanup Code removal, deprecation, refactorings, etc. kind: fix This fixes a bug or incorrect documentation. part: program
#19678 opened Oct 11, 2024 by SkySkimmer Loading… 9.0 rc1
4
Fix #19658 (spurious incompatible-prefix warning with recursive notations) kind: fix This fixes a bug or incorrect documentation. kind: user messages Improvement of error messages, new warnings, etc. part: notations The notation system.
#19673 opened Oct 10, 2024 by proux01 Loading…
2 tasks done
9.0 rc1
1
@herbelin
5
Ensure that the binder (x:T|P) does not depend on the implicit status of Specif.sig. 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.
#19670 opened Oct 9, 2024 by herbelin Loading… 9.0 rc1
5
[stdlib] made Fin.case_L_R' and Fin.case_L_R computational 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: standard library The standard library stdlib.
#19655 opened Oct 8, 2024 by mrhaandi Loading…
1 task done
Make the output of info_auto be the list of tactics it finds kind: usability Not a bug (fix) but a usability issue / improvement, e.g. UI or syntax inconsistencies needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. part: tactics
#19654 opened Oct 7, 2024 by jfehrle Loading…
1 of 3 tasks
9.0 rc1
13
Fix #19451 (spurious incompatible-prefix warning when using "as pattern") kind: fix This fixes a bug or incorrect documentation. kind: user messages Improvement of error messages, new warnings, 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: notations The notation system.
#19653 opened Oct 7, 2024 by proux01 Loading…
2 tasks done
9.0 rc1
1
@herbelin
4
Allow raw universes expressions (eg "Stdlib.Init.Logic.1") in Print Universes Subgraph kind: enhancement Enhancement to an existing user-facing feature, tactic, etc.
#19640 opened Oct 3, 2024 by SkySkimmer Loading… 9.0 rc1
@proux01
34
Print Universes print which constants caused a univ constraint 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. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run.
#19617 opened Sep 28, 2024 by SkySkimmer Loading…
14
[config] Re-enable use of configure option -bytecode-compiler kind: bug An error, flaw, fault or unintended behaviour. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19616 opened Sep 28, 2024 by ejgallego Loading… 9.0 rc1
3
Evarconv: save keys needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19611 opened Sep 27, 2024 by Tragicus Loading…
1 of 6 tasks
12
Fix collision with autogenerated universe names generate names for more global universes 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. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run.
#19599 opened Sep 23, 2024 by SkySkimmer Loading…
2
wip provide location info for defined objects needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19584 opened Sep 20, 2024 by SkySkimmer • Draft
5
Let post-processing of Derive statements take the same route as Definition and Theorem kind: cleanup Code removal, deprecation, refactorings, 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: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. part: derive request: full CI Use this label when you want your next push to trigger a full CI.
#19578 opened Sep 20, 2024 by herbelin • Draft 9.0 rc1
SSR pf_interp_ty use typing constraint instead of inserting cast needs: discussion Further discussion is needed.
#19543 opened Sep 13, 2024 by SkySkimmer Loading…
1
3
Algebraic universes everywhere and new constraint algorithm 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.
#19537 opened Sep 12, 2024 by mattam82 • Draft
6 tasks
1
Give Stdlib its own directory kind: infrastructure CI, build tools, development tools. part: standard library The standard library stdlib.
#19530 opened Sep 11, 2024 by proux01 Loading…
30 of 38 tasks
@CohenCyril
167
ProTip! Exclude everything labeled bug with -label:bug.