[go: up one dir, main page]
Skip to content

Pull requests: coq/coq

New pull request New
107 Open 9,610 Closed
107 Open 9,610 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

Avoid term_of_process whe possible in whd_betaiota_deltazeta_for_iota_state
#19850 opened Nov 18, 2024 by SkySkimmer • Draft
2
Use Vars.substituend in CClosure.comp_subs kind: performance Improvements to performance and efficiency. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19849 opened Nov 18, 2024 by SkySkimmer • Draft
1
Add test for template poly extracted from mtac2 kind: internal API, ML documentation...
#19848 opened Nov 18, 2024 by SkySkimmer Loading… 9.0+rc1
1
@ppedrot
Remove the unused PATTERNIDENT token. kind: cleanup Code removal, deprecation, refactorings, etc.
#19847 opened Nov 18, 2024 by ppedrot Loading… 9.0+rc1
Use reference nonterminal to parse references in terms kind: cleanup Code removal, deprecation, refactorings, etc.
#19846 opened Nov 18, 2024 by SkySkimmer Loading…
Fix binder factorization when implicit status differ kind: fix This fixes a bug or incorrect documentation. kind: user messages Error messages, warnings, etc.
#19845 opened Nov 18, 2024 by SkySkimmer Loading… 8.20.1
1
Stop adding user-contrib, xgd dirs and COQPATH to ml loadpath kind: cleanup Code removal, deprecation, refactorings, etc.
#19842 opened Nov 18, 2024 by SkySkimmer Loading… 9.0+rc1
coq_makefile stop installing cmxs files in legacy location kind: cleanup Code removal, deprecation, refactorings, etc. part: tools Coqdoc, coq_makefile, etc.
#19841 opened Nov 18, 2024 by SkySkimmer Loading… 9.0+rc1
2
Delay import of notation sets in Notationextern. kind: performance Improvements to performance and efficiency.
#19840 opened Nov 18, 2024 by ppedrot Loading… 9.0+rc1
1
rm problematic variables under beta redexes for evar instantiation needs: changelog entry This should be documented in doc/changelog. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19833 opened Nov 14, 2024 by Tragicus Loading…
6 tasks
7
When a record cannot be declared with primitive projections, explain why kind: user messages Error messages, warnings, etc.
#19831 opened Nov 13, 2024 by SkySkimmer Loading… 9.0+rc1
@ppedrot
3
Provide a way to associate a name with a Hint Extern needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19824 opened Nov 10, 2024 by jfehrle Loading…
4 tasks done
1
23
Show "autoapply" tactic for tc eauto debug; include dbnames in tactic for info where needed needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. part: tactics
#19823 opened Nov 10, 2024 by jfehrle Loading…
2 tasks done
1
3
rm problematic variables under beta-redexes and evars for evar instantiation needs: test-suite update Test case should be added to / updated in the test-suite.
#19822 opened Nov 9, 2024 by Tragicus Loading…
6 tasks
60
Remove "stdlib2" from CI kind: infrastructure CI, build tools, development tools.
#19820 opened Nov 8, 2024 by SkySkimmer Loading… 9.0+rc1
Debug print for lazy (wip) needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19814 opened Nov 7, 2024 by SkySkimmer • Draft
19
Update CODE_OF_CONDUCT.md needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19812 opened Nov 6, 2024 by tabareau Loading…
17
Better primitive projections handling in tactics and pretyper. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.
#19811 opened Nov 6, 2024 by jpoiret • Draft
1 of 4 tasks
1
removed uses and of Zeq_bool in setoid_ring
#19810 opened Nov 6, 2024 by ybertot • Draft
6 tasks
2
Create HintDb does not erase pre-existing hint db kind: fix This fixes a bug or incorrect documentation. needs: test-suite update Test case should be added to / updated in the test-suite.
#19808 opened Nov 5, 2024 by SkySkimmer Loading… 9.0+rc1
1
@ppedrot
9
Use the release Dune profile when running configure during opam package installation 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: build The build system.
#19805 opened Nov 4, 2024 by dra27 Loading… 9.0+rc1
@ejgallego
7
make Zeq_bool an alias for Z.eqb, deprecate ZArith_Base kind: cleanup Code removal, deprecation, refactorings, etc. needs: changelog entry This should be documented in doc/changelog. 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.
#19801 opened Nov 2, 2024 by andres-erbsen • Draft
16 of 17 tasks
9.0+rc1
25
ZMicromega does not depend on Q kind: cleanup Code removal, deprecation, refactorings, etc. part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic. part: standard library The standard library stdlib.
#19800 opened Nov 2, 2024 by andres-erbsen Loading…
1 task done
5
RFC: Split stdlib Program into Init and deprecated kind: cleanup Code removal, deprecation, refactorings, etc. needs: merge of dependency This PR depends on another PR being merged first. part: program part: standard library The standard library stdlib.
#19798 opened Oct 31, 2024 by andres-erbsen Loading…
5 tasks
3
use Program less in stdlib kind: cleanup Code removal, deprecation, refactorings, etc. needs: overlay This is breaking external developments we track in CI. part: program part: standard library The standard library stdlib.
#19797 opened Oct 31, 2024 by andres-erbsen Loading…
7
ProTip! Updated in the last three days: updated:>2024-11-15.