Skip to content

Pull requests: coq/coq

New pull request New
117 Open 9,062 Closed
117 Open 9,062 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

Use algebraic datatypes to signal failure in Conversion API kind: cleanup Code removal, deprecation, refactorings, etc.
#19120 opened May 30, 2024 by ppedrot Loading…
@SkySkimmer
6
Improve Ltac2 printing of glob exprs
#19119 opened May 30, 2024 by SkySkimmer Loading…
@ppedrot
Start a GoodDefaults file collecting recommended option settings. kind: compatibility Changes allowing for compatibility between versions. kind: feature New user-facing feature request or implementation. needs: changelog entry This should be documented in doc/changelog. needs: documentation Documentation was not added or updated. 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.
#19117 opened May 30, 2024 by Zimmi48 • Draft
2 tasks
8.20+rc1
10
Remove most deprecated coqlib.ml APIs
#19116 opened May 30, 2024 by SkySkimmer Loading…
@ppedrot
Use Coqlib for setoid_rewrite part: rewriting tactics The rewrite, autorewrite, rewrite_strat, and setoid_rewrite tactics.
#19115 opened May 30, 2024 by mattam82 Loading…
1 task done
@ppedrot
5
Using more often names of universes in universe inconsistency message, if possible kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: user messages Improvement of error messages, new warnings, 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. part: universes The universe system.
#19114 opened May 30, 2024 by herbelin Loading…
1 task done
8.20+rc1
4
Do not store transitively required kernel libraries on disk. kind: performance Improvements to performance and efficiency.
#19113 opened May 29, 2024 by ppedrot Loading… 8.20+rc1
10
dune-project: memtrace is a depopt kind: infrastructure CI, build tools, development tools.
#19112 opened May 29, 2024 by SkySkimmer Loading… 8.17.2
1
@Alizter
2
canonical structure hook needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19109 opened May 29, 2024 by Tragicus Loading…
3 tasks
2
Constrintern.ml support for setting "force" status of some implicit arguments 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.
#19108 opened May 28, 2024 by herbelin Loading… 8.20+rc1
Merging the code paths for fixpoint and cofixpoints 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: cofixpoints About CoFixpoint, cofix and mutual statements part: fixpoints About Fixpoint, fix and mutual statements
#19107 opened May 28, 2024 by herbelin Loading… 8.20+rc1
Removing the special case i=0 in declare_possibly_mutual_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.
#19106 opened May 28, 2024 by herbelin Loading… 8.20+rc1
2
Merging the code paths for interactive and non-interactive co/fixpoints kind: cleanup Code removal, deprecation, refactorings, etc. part: cofixpoints About CoFixpoint, cofix and mutual statements part: fixpoints About Fixpoint, fix and mutual statements
#19105 opened May 28, 2024 by herbelin Loading… 8.20+rc1
5
Delay universe conversion as late as possible in Reductionops.infer_conv. kind: experiment kind: performance Improvements to performance and efficiency.
#19104 opened May 28, 2024 by ppedrot • Draft
3
Ltac2: Avoid double typechecking in exact
#19102 opened May 28, 2024 by SkySkimmer Loading…
1
Fixes #19099: binders of universe polymorphic primitive constants treated as monomorphic kind: fix This fixes a bug or incorrect documentation. part: primitive types Primitive ints, floats, arrays, etc. part: universes The universe system.
#19100 opened May 27, 2024 by herbelin Loading…
2 tasks done
1
1
ppvernac fixes (univdecl incorrect printing and attribute spacing) 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.
#19095 opened May 27, 2024 by SkySkimmer Loading…
Better integration of Derive in declare.ml + removal of arbitrary restriction of Admitted to one statement + fix of #18951 kind: cleanup Code removal, deprecation, refactorings, etc. kind: enhancement Enhancement to an existing user-facing feature, tactic, 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: 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: derive
#19092 opened May 26, 2024 by herbelin Loading…
1 of 2 tasks
8.20+rc1
1
Use multiple statements to implement interactive fixpoints 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: cofixpoints About CoFixpoint, cofix and mutual statements part: fixpoints About Fixpoint, fix and mutual statements
#19091 opened May 26, 2024 by herbelin Loading… 8.20+rc1
4
Add support for Admitted on multiple statements kind: cleanup Code removal, deprecation, refactorings, etc. 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: gallina The gallina commands
#19090 opened May 26, 2024 by herbelin Loading… 8.20+rc1
1
Add optional type annotation to Derive 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: derive
#19087 opened May 25, 2024 by herbelin Loading… 8.20+rc1
12
Make CSet extensible on our side, and adding CSet.List.union. kind: cleanup Code removal, deprecation, refactorings, etc. needs: progress Work in progress: awaiting action from the author.
#19075 opened May 23, 2024 by herbelin Loading… 8.20+rc1
12
Univ declarations can have extensible qualities (internally) kind: fix This fixes a bug or incorrect documentation.
#19073 opened May 22, 2024 by SkySkimmer Loading… 8.20+rc1
1
@ppedrot
5
Move enforce_locality_exp definition and calling to DefAttributes kind: cleanup Code removal, deprecation, refactorings, etc.
#19068 opened May 22, 2024 by SkySkimmer Loading…
@ppedrot
4
Slightly more straightforward implementation of Equality.decomp_tuple_term kind: cleanup Code removal, deprecation, refactorings, etc.
#19061 opened May 21, 2024 by ppedrot Loading… 8.20+rc1
ProTip! Add no:assignee to see everything that’s not assigned.