[go: nahoru, domu]
Skip to content

Pull requests: coq/coq

New pull request New
Clear current search query, filters, and sorts
105 Open 9,235 Closed
105 Open 9,235 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

Clean-up include module syntax. kind: cleanup Code removal, deprecation, refactorings, etc. 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. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run.
#11897 opened Mar 24, 2020 by Zimmi48 • Draft
1 of 3 tasks
19
[build] Add support for code coverage help wanted 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. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. needs: squashing Some commits should be squashed together. needs: test-suite update Test case should be added to / updated in the test-suite. part: build The build system.
#12259 opened May 6, 2020 by ejgallego • Draft
1
@SkySkimmer
113
Fixes #5698: let simpl grants the never flag for primitive projections independently of the internal unfolded status kind: cleanup Code removal, deprecation, refactorings, etc. 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. 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. part: primitive records The primitive record and primitive projection mechanism. part: reduction strategies The Strategy command for defining reduction straegies.
#15661 opened Feb 10, 2022 by herbelin Loading…
3 tasks done
1
20
[coqdep] Don't "canonize" files. kind: cleanup Code removal, deprecation, refactorings, etc. needs: changelog entry This should be documented in doc/changelog. part: coqdep The coqdep binary for resolving dependencies amongst coq .v files.
#16116 opened May 31, 2022 by ejgallego Loading…
7
Simple compiler for benchmark needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#16190 opened Jun 15, 2022 by ejgallego • Draft
77
Allow Ltac2 notations from within Ltac1 kind: feature New user-facing feature request or implementation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
#16394 opened Aug 18, 2022 by ppedrot • Draft
3 tasks
27
[stdlib] Add Proper instances for some number theorems to improve rewriting with inequalities kind: feature New user-facing feature request or implementation. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. part: standard library The standard library stdlib. stale This PR will be closed unless it is rebased.
#16792 opened Nov 11, 2022 by haansn08 Loading… 8.21+rc1
39
[RFC WIP] fast extensional finite maps in theories/EMaps/Trie.v 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.
#17044 opened Dec 30, 2022 by andres-erbsen • Draft
3 tasks
1
Make interpretation of references with maximal implicit arguments in Ltac functions the same in strict and non-strict mode kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. needs: changelog entry This should be documented in doc/changelog. needs: progress Work in progress: awaiting action from the author. part: ltac Issues and PRs related to the Ltac tactic language.
#17084 opened Jan 7, 2023 by herbelin Loading…
2 tasks
10
Add reg theorems for nat on multiplication needs: changelog entry This should be documented in doc/changelog. part: standard library The standard library stdlib.
#17560 opened May 2, 2023 by HaoYang670 Loading… 8.21+rc1
1
@andres-erbsen
17
[stdlib] remove things deprecated in 8.17 kind: cleanup Code removal, deprecation, refactorings, etc. needs: overlay This is breaking external developments we track in CI. part: standard library The standard library stdlib.
#17700 opened Jun 7, 2023 by andres-erbsen Loading…
3 tasks
15
Experiment to preserve information from typeclass failures 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. 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. part: typeclasses The typeclass mechanism. stale This PR will be closed unless it is rebased.
#17701 opened Jun 7, 2023 by SkySkimmer • Draft
7
[stdlib] decidability of Nat.divide 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.
#17820 opened Jul 5, 2023 by haansn08 Loading…
6
Add gramlib support for non-associativity and for deactivating the recovery mode 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: parser
#17876 opened Jul 20, 2023 by herbelin • Draft
11
[DRAFT] Add PrimFloat.fma 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. 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. part: primitive types Primitive ints, floats, arrays, etc.
#17900 opened Jul 28, 2023 by JasonGross • Draft
2 of 3 tasks
1
3
[release] script to publish opam packages kind: infrastructure CI, build tools, development tools. kind: meta About the process of developing Coq. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#17921 opened Aug 3, 2023 by gares Loading…
8
More appropriately moving PropExt->ProofIrrel to file PropExtensionalityFact.v part: standard library The standard library stdlib.
#18092 opened Sep 28, 2023 by herbelin Loading…
13
Ltac2: named type variables can't be defined kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
#18118 opened Oct 3, 2023 by SkySkimmer Loading…
8
[stdlib] well-founded list extension 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.
#18183 opened Oct 19, 2023 by mrhaandi Loading…
1 task done
3
Doc: move prodn for filtered_import and import_categories 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.
#18295 opened Nov 10, 2023 by SkySkimmer Loading…
7
Fix #18332 (specialize does not support evars in the instantiated args) needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#18341 opened Nov 21, 2023 by Matafou Loading…
@ppedrot
26
[build] Remove the legacy loading mode. kind: cleanup Code removal, deprecation, refactorings, etc. needs: changelog entry This should be documented in doc/changelog. needs: fixing The proposed code change is broken. needs: squashing Some commits should be squashed together. part: build The build system.
#18385 opened Dec 7, 2023 by ejgallego Loading…
32
Ltac2: a fail returning 'a instead of unit and accepting printf-style arguments needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. needs: squashing Some commits should be squashed together.
#18420 opened Dec 19, 2023 by samuelgruetter Loading…
2 tasks done
1
9
More uniform support for maximal implicit arguments and multiple blocks of implicit arguments in notations, including a fix to #3516 (improved Print for abbreviations aliasing a name) 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: implicit arguments The implicit arguments mechanism, generalizable variables, etc. part: printer The printing mechanism of Coq.
#18446 opened Dec 30, 2023 by herbelin Loading…
2 tasks done
1
7
Remove include type 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: modules The module system of Coq.
#18482 opened Jan 10, 2024 by Villetaneuse • Draft 8.21+rc1
11
ProTip! Filter pull requests by the default branch with base:master.