Skip to content

Pull requests: LPCIC/coq-elpi

New pull request New
34 Open 785 Closed
34 Open 785 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

enable fresh qvar in primproj to see prblem in MC
#1063 opened Jul 6, 2026 by gares Contributor • Draft
Partial support for mutual inductives in derive
#1056 opened Jun 24, 2026 by Janno Contributor • Draft
10
Check existence of TC predicate before make class queries/rules
#1055 opened Jun 21, 2026 by FissoreD Collaborator Loading…
1
Plugin tuto
#1052 opened Jun 19, 2026 by FissoreD Collaborator Loading…
1
WIP: canonical structures compilation
#1045 opened Jun 16, 2026 by FissoreD Collaborator • Draft
Add test case for recompilation bug with sections
#1043 opened Jun 15, 2026 by Janno Contributor • Draft
Add builtin to the tc app
#1042 opened Jun 12, 2026 by Tragicus Contributor • Draft
17
Fix phase separation for lib:qid syntax
#1035 opened Jun 8, 2026 by SkySkimmer Collaborator • Draft
Switch from [coq.theory] to [rocq.theory].
#1033 opened Jun 5, 2026 by rlepigre-skylabs-ai Contributor Loading…
9
pglobals: add hole for universe level
#1019 opened May 12, 2026 by FissoreD Collaborator • Draft
Adapt to https://github.com/rocq-prover/stdlib/pull/251
#998 opened Apr 13, 2026 by proux01 Contributor • Draft
Adapt to rocq-prover/rocq#21773 (sort polymorphic cumulativity)
#982 opened Mar 18, 2026 by SkySkimmer Collaborator • Draft
fix a bunch of warnings
#980 opened Mar 17, 2026 by gares Contributor Loading…
Name holes in detyping
#925 opened Nov 6, 2025 by Tragicus Contributor Loading…
1
8
quantify over universes in build iota
#904 opened Oct 12, 2025 by patrick-nicodemus Contributor Loading…
22
Adapt to rocq-prover/rocq#21098
#899 opened Oct 6, 2025 by gares Contributor • Draft
Add support for syntactic command arguments
#893 opened Sep 26, 2025 by Janno Contributor • Draft
1 task
4
Allow accumulating Dbs (and other things) into Dbs
#890 opened Sep 23, 2025 by Janno Contributor • Draft
1 task
1
Close to working tabled type class
#861 opened Aug 7, 2025 by cmester0 Loading…
11
Universes clauses
#841 opened Jun 26, 2025 by CohenCyril Collaborator Loading…
3
[tc] attribute parser for the creation of elpi predicates for tc
#709 opened Oct 28, 2024 by FissoreD Collaborator Loading…
1
Adapt to Coq PR #19301 which unifies the syntax of Theorem, Definition and Fixpoint
#703 opened Oct 24, 2024 by herbelin Contributor Loading…
2
Elpi Compile to fill the cache
#694 opened Sep 24, 2024 by gares Contributor Loading…
1
Adapt to Coq PR #19404: an algebra of types for the instances of notation variables
#673 opened Jul 21, 2024 by herbelin Contributor Loading…
8
Fix roots in solution2evd
#614 opened Mar 19, 2024 by Tragicus Contributor Loading…
7
ProTip! Adding no:label will show everything without a label.