[go: nahoru, domu]
Skip to content

Pull requests: coq/coq

New pull request New
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

Fix #18572: tactic clear sometimes too eager to remove a dependency in an existential variable vs restricting the context of the existential variable kind: fix This fixes a bug or incorrect documentation. needs: fixing The proposed code change is broken. part: existential variables Existential variables, also known as evars, represent as yet unknown values in a proof. part: tactics
#18617 opened Feb 3, 2024 by herbelin Loading…
2 tasks done
8.21+rc1
1
@SkySkimmer
46
Declare global sort variables 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. part: universes The universe system. part: vernac High level command interpretation.
#18615 opened Feb 2, 2024 by kyoDralliam • Draft
6 tasks
@SkySkimmer
8
Take "simpl never" into account for "simpl" in position of argument of a "match", "fix" or projection 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: 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: reduction strategies The Strategy command for defining reduction straegies. part: tactics
#18581 opened Jan 28, 2024 by herbelin Loading…
1 of 2 tasks
17
Do not use "simpl never" and cie in "hnf" kind: fix This fixes a bug or incorrect documentation. part: reduction strategies The Strategy command for defining reduction straegies. part: tactics
#18580 opened Jan 28, 2024 by herbelin Loading…
2 tasks done
8.21+rc1
16
Clarify the status of the independence of general premises in file ClassicalFacts.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.
#18575 opened Jan 27, 2024 by herbelin Loading…
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
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
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
[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
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
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
[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
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
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
[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
[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
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
[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
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] 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
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
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
[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
[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
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
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.