Skip to content

Pull requests: rocq-prover/rfcs

New pull request New
54 Open 51 Closed
54 Open 51 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
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Elimination constraints for bounded sort polymorphism
#111 opened Sep 26, 2025 by jrosain Loading…
2
Debugging generalized rewriting tactics
#110 opened Jul 7, 2025 by radrow Loading…
1
Multiple Default Typeclass Databases
#109 opened Jul 2, 2025 by Janno • Draft
10
Indentation based bullet behavior
#108 opened Jun 30, 2025 by proux01 Loading…
37
Asserting outputs of vernacular commands and tactics
#107 opened Jun 4, 2025 by radrow Loading…
12
Named notation levels
#106 opened Jun 3, 2025 by proux01 Loading…
28
Reduction
#105 opened Feb 13, 2025 by Janno • Draft
18
Rocq Package Metadata: Piggybacking on Findlib.
#101 opened Nov 11, 2024 by rlepigre Loading…
15
A Compilation of Short Interactive Tutorials and How-To Guides for Coq
#91 opened Jun 20, 2024 by thomas-lamiaux Loading…
30
Template poly redesign using sort poly
#90 opened May 21, 2024 by SkySkimmer Loading…
12
A unique execution path for the treatement of universes in declare.ml
#89 opened May 20, 2024 by herbelin Loading…
1
Abstract ("side effects") redesign (WIP)
#88 opened May 16, 2024 by SkySkimmer • Draft
Reduce barriers to contributing to the standard library
#86 opened Apr 12, 2024 by andres-erbsen Loading…
14
Enriched and unified syntax for reduction strategies
#85 opened Feb 9, 2024 by herbelin Loading…
6
Added new CEP Symbol Sets
#84 opened Feb 6, 2024 by MSoegtropIMC Loading…
5
Boost stdlib development
#83 opened Feb 6, 2024 by proux01 Loading…
159
Rocq Object Metadata
#80 opened Dec 18, 2023 by CohenCyril Loading…
6
Adding a CEP about Reals
#74 opened Sep 15, 2023 by Villetaneuse Loading…
23
Giving access in match to the expansion of the term being matched via an alias in order to support more fixpoints
#73 opened Aug 10, 2023 by herbelin Loading…
4
Discharge on the fly
#72 opened Jul 31, 2023 by herbelin Loading…
5
Towards a more flexible and accurate model for grammar levels and associativity
#71 opened Jul 22, 2023 by herbelin Loading…
6
Short-term roadmap for Coq
#69 opened Jul 17, 2023 by Zimmi48 • Draft
56
[CEP] Proposal for libobject API refactoring
#65 opened Sep 12, 2022 by ejgallego Loading…
14
Requirements for supporting Ltac2 debugging with a high-level outline of changes
#64 opened Apr 11, 2022 by jfehrle Loading…
11
Incremental Include
#63 opened Feb 15, 2022 by gmalecha Loading…
14
ProTip! Type g i on any issue or pull request to go back to the issue listing page.