-
Notifications
You must be signed in to change notification settings - Fork 54
Issues: LPCIC/coq-elpi
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.
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Emit
unexpected-implicit-declaration
warning on ignored implicit binders
#342
opened Feb 28, 2022 by
Blaisorblade
[derive] specialize foo.induction passing the result of derive.is_full
#264
opened Jul 11, 2021 by
gares
@pi-decl "x" Ty x\ foo {{ f a }}
does not work well if f has implicits
#316
opened Dec 10, 2021 by
gares
@local! => coq.env.add-const
does not support local definitions
#374
opened Jul 22, 2022 by
Blaisorblade
coq.env.add-indt fails to add universe polymorphic inductives when not in a section
#387
opened Sep 1, 2022 by
ecranceMERCE
derive should generate functoriality properties for param1 translation of non-inductive predicates
#426
opened Jan 19, 2023 by
adelaett
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
Previous Next
ProTip!
no:milestone will show everything without a milestone.