Skip to content

Pull requests: LPCIC/coq-elpi

New pull request New
29 Open 670 Closed
29 Open 670 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

Adapt to rocq-prover/rocq#21195 (Constraints->UnivConstraints, univ_decl->sort_poly_decl)
#934 opened Nov 24, 2025 by TDiazT Loading…
Adapt to rocq-prover/rocq#21342 (grammar extensions can avoid adding keywords)
#933 opened Nov 24, 2025 by SkySkimmer • Draft
Adapt to rocq-prover/rocq#21342 (removed "raw" field in printing flags)
#932 opened Nov 21, 2025 by SkySkimmer • Draft
Name holes in detyping
#925 opened Nov 6, 2025 by Tragicus Loading…
1
8
Test for fix type name collision
#908 opened Oct 17, 2025 by gares • Draft
quantify over universes in build iota
#904 opened Oct 12, 2025 by patrick-nicodemus Loading…
22
Adapt to rocq-prover/rocq#21098
#899 opened Oct 6, 2025 by gares • Draft
Fix bug in tc.compile.goal.decompile-problematic-term
#896 opened Oct 3, 2025 by Tragicus Loading…
Add support for syntactic command arguments
#893 opened Sep 26, 2025 by Janno • Draft
1 task
4
Allow accumulating Dbs (and other things) into Dbs
#890 opened Sep 23, 2025 by Janno • Draft
1 task
1
Indexing in coercion and tc
#886 opened Sep 12, 2025 by Tragicus • Draft
Close to working tabled type class
#861 opened Aug 7, 2025 by cmester0 Loading…
11
Universes clauses
#841 opened Jun 26, 2025 by CohenCyril Loading…
3
TC Solver: prim-proj and canonical struct
#802 opened Apr 8, 2025 by FissoreD • Draft
@FissoreD
[tc] attribute parser for the creation of elpi predicates for tc
#709 opened Oct 28, 2024 by FissoreD Loading…
1
Adapt to Coq PR #19301 which unifies the syntax of Theorem, Definition and Fixpoint
#703 opened Oct 24, 2024 by herbelin Loading…
2
Elpi Compile to fill the cache
#694 opened Sep 24, 2024 by gares Loading…
1
Adapt to Coq PR #19404: an algebra of types for the instances of notation variables
#673 opened Jul 21, 2024 by herbelin Loading…
1
[TC] CS projections replaced with uvar
#648 opened Jul 2, 2024 by FissoreD Loading…
4
Fix roots in solution2evd
#614 opened Mar 19, 2024 by Tragicus Loading…
7
Cswb
#591 opened Feb 8, 2024 by Tragicus Loading…
4
Supporting no purge of algebraic universes
#585 opened Feb 1, 2024 by CohenCyril Loading…
10
Update apps/tc/README.md
#568 opened Jan 4, 2024 by gares • Draft
3 of 10 tasks
1
Missing API on universes
#544 opened Nov 11, 2023 by CohenCyril Loading…
4
add predicates to coq-lib to convert elpi strings and lists to coq strings and lists.
#530 opened Oct 31, 2023 by lukovdm Loading…
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.