Skip to content

Issues: LPCIC/coq-elpi

Beta
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

63 Open 143 Closed
63 Open 143 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
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
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Section variable leak
#830 opened May 27, 2025 by Tragicus
3
rename variable even if not colliding
#821 opened May 15, 2025 by gares
1
Modes ignored on recursive typeclass search
#815 opened Apr 28, 2025 by Tragicus
2
TC not resilient to small changes deep in a term
#798 opened Apr 8, 2025 by Tragicus
Quoted terms do not use primitive projections
#797 opened Apr 7, 2025 by Tragicus
1
Inconsistency with complex command arguments
#760 opened Jan 28, 2025 by yannl35133
3
whd-indc does not support pglobal
#756 opened Jan 27, 2025 by patrick-nicodemus
7
Issue with refine
#755 opened Jan 26, 2025 by patrick-nicodemus
4
Elpi Db mydb lp:{{ <code> }} not the same as Elpi Db mydb lp:{{ }}. Elpi Accumulate mydb lp:{{ <code> }}
#721 opened Nov 28, 2024 by Janno
10
wish: coq.env.add-* could typecheck by default
#710 opened Oct 29, 2024 by gares
Elpi Query fails if (a useless) evar is assigned a term not in HOAS
#691 opened Sep 18, 2024 by gares
Feature request: Remove dependence of elpi on stdlib
#677 opened Aug 4, 2024 by patrick-nicodemus
6
Improve translation in HOAS tutorial
#676 opened Aug 4, 2024 by patrick-nicodemus
Weird behaviour of reduction of coq terms bug
#639 opened Jun 19, 2024 by FissoreD
4
Db sharing between synterp and interp
#622 opened Apr 17, 2024 by trilis
1
The interp implementation of coq.env.current-section-path uses a synterp-specific API
#606 opened Feb 29, 2024 by rlepigre
Homebrew TC algorithm breaks evar map invariants
#578 opened Jan 25, 2024 by ppedrot
5
Increase timeout in test that takes a bit longer on riscv64
#576 opened Jan 24, 2024 by SnarkBoojum
missing glob info for notations
#575 opened Jan 24, 2024 by gares
2
coq.env.add-indt not preserving implicit arguments
#574 opened Jan 23, 2024 by FissoreD
delegating a proof containing elpi tactic raises Nout_found (STM)
#558 opened Dec 4, 2023 by gares
Add clauses immediately after predicate declaration
#546 opened Nov 14, 2023 by Tragicus
1
Strange VsCoq Legacy anomaly with Elpi Export
#543 opened Nov 10, 2023 by trilis
11
Anomaly "in retype: Not an arity" when coercing from a structure to sig
#532 opened Nov 3, 2023 by Tragicus
4
A failure of derive.param1 with template polymorphism in Prop
#527 opened Oct 24, 2023 by herbelin
ProTip! Find all open issues with in progress development work with linked:pr.