Skip to content

Pull requests: coq/coq

New pull request New
128 Open 8,997 Closed
128 Open 8,997 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

Adding change log for PR #18873 (anomaly instead of error on missing obligation of some name)
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. part: program
#19057 opened May 20, 2024 by herbelin Loading… 8.20+rc1
[CI] Bump ci-jasmin
kind: infrastructure CI, build tools, development tools. part: CI The continuous integration system.
#19056 opened May 20, 2024 by JasonGross Loading… 8.20+rc1
6
Restrict check_conv_problems in pretyping to those problems referring to the term to type
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: tactics
#19054 opened May 19, 2024 by herbelin • Draft
1 of 2 tasks
8.20+rc1
4
coq_interp: squelch a incompatible-pointer warning
needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19052 opened May 19, 2024 by artagnon Loading…
Fix wrapping of guard error with evar map in cofix guard checking
needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19051 opened May 19, 2024 by SkySkimmer Loading…
1
Code factorization around Evarutil.finalize and prepare_obligations
kind: cleanup Code removal, deprecation, refactorings, etc. part: universes The universe system.
#19050 opened May 17, 2024 by herbelin Loading…
1 task
8.20+rc1
1
[notations] Warn about incompatible prefixes
kind: user messages Improvement of error messages, new warnings, etc. part: notations The notation system.
#19049 opened May 17, 2024 by proux01 Loading…
4 of 6 tasks
8.20+rc1
15
[experiment] Skip conversion of lambda annotations with a common supertype, the return
needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19048 opened May 17, 2024 by ppedrot • Draft
3
Fix debug printing of Lambda projections.
kind: internal API, ML documentation...
#19046 opened May 17, 2024 by ppedrot Loading… 8.20+rc1
@SkySkimmer
Small code factorization of qvar generation in pretyping
kind: cleanup Code removal, deprecation, refactorings, etc.
#19045 opened May 17, 2024 by SkySkimmer Loading… 8.20+rc1
@ppedrot
1
Print qvar names in Show Universes / ocamldebug ustate printer
kind: user messages Improvement of error messages, new warnings, etc.
#19044 opened May 17, 2024 by SkySkimmer Loading… 8.20+rc1
@ppedrot
2
Fix handling of sort poly squash in typing.ml
#19042 opened May 17, 2024 by SkySkimmer Loading…
1
@ppedrot
1
Fix passing line number of errors in xml protocol, causing ill-located or non-located errors, notably in the presence of utf8 characters
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: xml protocol
#19040 opened May 17, 2024 by herbelin Loading…
1 task done
8.20+rc1
1
9
Additions to String module and extraction to OCaml native strings
needs: changelog entry This should be documented in doc/changelog. part: standard library The standard library stdlib.
#19037 opened May 16, 2024 by BridgeTheMasterBuilder Loading…
1 of 4 tasks
10
More efficient compilation of PArray blobs in the VM.
kind: performance Improvements to performance and efficiency.
#19034 opened May 16, 2024 by ppedrot • Draft
8
added ltac2 bindings for congruence and simple congruence
needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19032 opened May 15, 2024 by StamesJames Loading…
26
Towards a common execution path for universe restriction + universe declaration check
kind: cleanup Code removal, deprecation, refactorings, etc. needs: merge of dependency This PR depends on another PR being merged first. part: universes The universe system.
#19031 opened May 15, 2024 by herbelin • Draft 8.20+rc1
Remove useless typechecking of future goals in refine
#19030 opened May 15, 2024 by SkySkimmer Loading…
3
Experiment the addition of sealed/unsealed attributes
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: attributes #[attributes] modify the behaviour of vernac sentences. part: gallina The gallina commands
#19029 opened May 15, 2024 by herbelin • Draft
3 tasks
8.20+rc1
Remove the cutrewrite tactic.
kind: cleanup Code removal, deprecation, refactorings, etc. needs: changelog entry This should be documented in doc/changelog.
#19027 opened May 15, 2024 by ppedrot Loading… 8.20+rc1
3
[8.20] Update compat infrastructure prior to branching
kind: cleanup Code removal, deprecation, refactorings, etc.
#19026 opened May 15, 2024 by proux01 Loading… 8.20+rc1
@silene
8
Prevent useless typing in Equality.subst_tuple_term
needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19024 opened May 14, 2024 by ppedrot • Draft
5
abstract:{ tactic block
needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19023 opened May 14, 2024 by SkySkimmer • Draft
3
Fix incorrect handling of Elimination and Case schemes
kind: fix This fixes a bug or incorrect documentation.
#19017 opened May 13, 2024 by SkySkimmer Loading… 8.20+rc1
1
@ppedrot
7
Track unused constant arguments in Genlambda and erase them.
kind: performance Improvements to performance and efficiency. part: native compiler part: VM Virtual machine.
#19014 opened May 11, 2024 by ppedrot Loading… 8.20+rc1
@SkySkimmer
24
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.