[go: nahoru, domu]
Skip to content

Pull requests: coq/coq

New pull request New
102 Open 9,221 Closed
102 Open 9,221 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

Above-prop-below-type
#19308 opened Jul 2, 2024 by yannl35133 Loading…
6 tasks
2
[gen_rules] option -dep to depend on other theories kind: infrastructure CI, build tools, development tools. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. part: build The build system.
#19307 opened Jul 2, 2024 by gares Loading… 8.21+rc1
9
Algorithmically faster computation of argument scopes. kind: fix This fixes a bug or incorrect documentation.
#19305 opened Jul 2, 2024 by ppedrot Loading… 8.20.0
1
@SkySkimmer
7
Experimenting beta-reducing terms displayed in some unification error messages kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. 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: unification The unification mechanism.
#19303 opened Jul 2, 2024 by herbelin Loading… 8.21+rc1
4
Ltac2 bindings for ssr needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19302 opened Jul 2, 2024 by gares • Draft
Unifying the syntax of Definition, Theorem, Fixpoint and CoFixpoint (CEP #42) kind: feature New user-facing feature request or implementation. 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. part: cofixpoints About CoFixpoint, cofix and mutual statements part: fixpoints About Fixpoint, fix and mutual statements part: gallina The gallina commands
#19301 opened Jul 2, 2024 by herbelin Loading…
3 tasks
8.21+rc1
Quickfix for deprecated 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.
#19300 opened Jul 1, 2024 by gares Loading…
1 task
8.21+rc1
Add devShell to flake.nix to allow nix-direnv to work needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19298 opened Jul 1, 2024 by Arya-Elfren Loading…
3
Avoid duplicate hashconsing of kerpairs needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19297 opened Jul 1, 2024 by SkySkimmer • Draft
2
Fixes #7913: fixpoint with decreasing argument hidden behind a definition kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: fix This fixes a bug or incorrect documentation. needs: fixing The proposed code change is broken. needs: merge of dependency This PR depends on another PR being merged first. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. part: fixpoints About Fixpoint, fix and mutual statements
#19296 opened Jun 30, 2024 by herbelin • Draft
1 of 2 tasks
8.21+rc1
1
Extend Derive with an arbitrary long sequence of dependencies 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: merge of dependency This PR depends on another PR being merged first. part: derive
#19295 opened Jun 30, 2024 by herbelin Loading…
3 tasks done
8.21+rc1
20
Avoid calling global_vars_set in constant_typing when not in section needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19291 opened Jun 28, 2024 by SkySkimmer Loading…
2
Proper RR typechecker needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run.
#19290 opened Jun 27, 2024 by yannl35133 • Draft
6 tasks
Ensure that andb_true_intro and andb_prop are transparent so that Scheme Equality computes kind: fix This fixes a bug or incorrect documentation. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. part: scheme The Scheme command for generating induction and equality schemes.
#19287 opened Jun 27, 2024 by herbelin Loading…
1 of 2 tasks
7
Changelog for 8.20 needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19281 opened Jun 27, 2024 by proux01 • Draft 8.20.0
@proux01
15
[CoqIDE] Display warnings in their own tab. kind: fix This fixes a bug or incorrect documentation.
#19272 opened Jun 25, 2024 by ppedrot Loading… 8.21+rc1
@jfehrle
5
Skip existential variable instances in Set Keep Admitted 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: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. part: proof engine part: sections The section mechanism of Coq.
#19270 opened Jun 24, 2024 by herbelin Loading…
1 of 3 tasks
8.21+rc1
2
[ci] update elpi branch kind: infrastructure CI, build tools, development tools. part: CI The continuous integration system.
#19268 opened Jun 24, 2024 by gares • Draft 8.20.0
21
Fix About info about squashing kind: fix This fixes a bug or incorrect documentation. kind: user messages Improvement of error messages, new warnings, etc.
#19266 opened Jun 24, 2024 by SkySkimmer Loading…
3
Move code for interactive definitions close to the one for non interactive definitions 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: merge of dependency This PR depends on another PR being merged first. part: gallina The gallina commands
#19260 opened Jun 22, 2024 by herbelin Loading… 8.21+rc1
Merge the code paths for "CoFixpoint"/"Fixpoint" and "Theorem with" kind: cleanup Code removal, deprecation, refactorings, etc. needs: merge of dependency This PR depends on another PR being merged first. part: cofixpoints About CoFixpoint, cofix and mutual statements part: fixpoints About Fixpoint, fix and mutual statements part: gallina The gallina commands
#19259 opened Jun 22, 2024 by herbelin Loading…
1 task done
8.21+rc1
8
Slightly improve -profile output
#19240 opened Jun 19, 2024 by SkySkimmer Loading…
1
Do not create global constraints for applied template polymorphic types
#19228 opened Jun 18, 2024 by ppedrot • Draft
71
[ci] [bench] CI / Bench for OCaml 5.2.0+trunk needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. part: ocaml
#19225 opened Jun 18, 2024 by ejgallego • Draft
17
Quickfix for intros 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.
#19224 opened Jun 18, 2024 by gares • Draft 8.21+rc1
1
ProTip! Updated in the last three days: updated:>2024-06-29.