Pull requests: coq/coq
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
Add SSReflect contextual pattern Additions or improvement to documentation.
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: ssreflect
The SSReflect proof language.
UNDER
kind: documentation
#19011
opened May 8, 2024 by
erikmd
Loading…
3 tasks done
Ltac2: runtime representation of univ instance is the raw instance
kind: cleanup
Code removal, deprecation, refactorings, etc.
[declare] Warn on unused using attributes on sub-obligations
needs: full CI
The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
Deprecate non-reference hints in using clauses of auto-like tactics.
kind: cleanup
Code removal, deprecation, refactorings, etc.
Handle Implicit Type for identonly binders in notations
#19003
opened May 6, 2024 by
SkySkimmer
Loading…
Phrasing and formatting of the unsatisfiable constraints error message
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: typeclasses
The typeclass mechanism.
[declare] Call interp_proof_using only once per mutual block.
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.
Remove the tag branch information from case_info.
kind: cleanup
Code removal, deprecation, refactorings, etc.
Warn when automatically lowering an inductive declared with 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: inductives
Inductive types, fixpoints, etc.
: Type to Prop
kind: enhancement
Add Fixpoint and CoFixpoint in Search logical_kind
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: search
Search and Locate vernac commands.
#18983
opened Apr 27, 2024 by
Villetaneuse
Loading…
4 of 6 tasks
Support syntax Enhancement to an existing user-facing feature, tactic, etc.
part: parser
part: sort polymorphism
The sorts subsystem of the universe system.
part: universes
The universe system.
Type@{q | _}
kind: enhancement
[wip] Incorrect experiment to clean up some code in the stm
kind: cleanup
Code removal, deprecation, refactorings, etc.
needs: discussion
Further discussion is needed.
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.
part: STM
State Transition Machine, asynchronous proofs, etc.
Add primitive string type.
needs: full CI
The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#18973
opened Apr 24, 2024 by
rlepigre
Loading…
1 of 4 tasks
experiment: measure gc time with ocaml 5 runtime events in newprofile
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.
#18972
opened Apr 23, 2024 by
SkySkimmer
•
Draft
Cleanup counter handling in newprofile
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.
#18970
opened Apr 23, 2024 by
SkySkimmer
Loading…
Add a PUSHACCMANY opcode.
kind: performance
Improvements to performance and efficiency.
part: VM
Virtual machine.
#18967
opened Apr 23, 2024 by
silene
Loading…
Fix occurrence checker not checking evar insts
help wanted
#18966
opened Apr 22, 2024 by
yannl35133
Loading…
Add a PUSHENVACCMANY opcode.
kind: performance
Improvements to performance and efficiency.
part: VM
Virtual machine.
#18964
opened Apr 22, 2024 by
silene
Loading…
Apply the early check of the universe declaration and the monomorphic universe fixing to all interactive declarations
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: fixpoints
About Fixpoint, fix and mutual statements
part: program
Compress the compiled bytecode.
kind: performance
Improvements to performance and efficiency.
needs: rebase
Should be rebased on the latest master to solve conflicts or have a newer CI run.
part: VM
Virtual machine.
#18959
opened Apr 19, 2024 by
silene
Loading…
Do not rely on floating universes in the upper layers
kind: cleanup
Code removal, deprecation, refactorings, etc.
Allow open terms in "apply ->" and "apply <-" (fix #18177).
kind: enhancement
Enhancement to an existing user-facing feature, tactic, etc.
part: ltac
Issues and PRs related to the Ltac tactic language.
#18946
opened Apr 17, 2024 by
silene
Loading…
2 of 3 tasks
autobuild .merlin files in CI scripts for some plugins
kind: infrastructure
CI, build tools, development tools.
#18941
opened Apr 17, 2024 by
SkySkimmer
Loading…
Return canonical instance from basic declare.ml APIs + use to fix Program bug
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: rebase
Should be rebased on the latest master to solve conflicts or have a newer CI run.
#18931
opened Apr 15, 2024 by
SkySkimmer
Loading…
Previous Next
ProTip!
Type g p on any issue or pull request to go back to the pull request listing page.