Skip to content

Pull requests: coq/rfcs

New pull request New
Clear current search query, filters, and sorts
46 Open 43 Closed
46 Open 43 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

Reduction
#105 opened Feb 13, 2025 by Janno • Draft
15
Rocq Package Metadata: Piggybacking on Findlib.
#101 opened Nov 11, 2024 by rlepigre • Review required
15
A Compilation of Short Interactive Tutorials and How-To Guides for Coq
#91 opened Jun 20, 2024 by thomas-lamiaux • Review required
30
Template poly redesign using sort poly
#90 opened May 21, 2024 by SkySkimmer • Review required
12
A unique execution path for the treatement of universes in declare.ml
#89 opened May 20, 2024 by herbelin • Review required
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 • Review required
9
Enriched and unified syntax for reduction strategies
#85 opened Feb 9, 2024 by herbelin • Review required
6
Added new CEP Symbol Sets
#84 opened Feb 6, 2024 by MSoegtropIMC • Review required
5
Boost stdlib development
#83 opened Feb 6, 2024 by proux01 Loading…
158
initial commit for the metadata CEP
#80 opened Dec 18, 2023 by CohenCyril Loading…
1
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
Incremental Include
#63 opened Feb 15, 2022 by gmalecha Loading…
14
Separate compilation
#62 opened Feb 14, 2022 by gmalecha Loading…
34
Proposal for unifying the syntax for parameters and indices of inductive types
#60 opened Oct 3, 2021 by herbelin Loading…
37
Unification structure
#59 opened Aug 31, 2021 by herbelin Loading…
23
A few propositions about the module system
#58 opened Aug 29, 2021 by herbelin Loading…
13
Document on primitive projections
#57 opened Aug 1, 2021 by herbelin Loading…
44
Subsingleton elimination and impredicativity for SProp, Prop and hProp
#55 opened Mar 4, 2021 by herbelin Loading…
31
Proposing to associate a qualified name to section variables so as to distinguish them from (other) goal variables
#51 opened Dec 9, 2020 by herbelin Loading…
20
ProTip! Exclude everything labeled bug with -label:bug.