Search results

Wrong .glob offsets for references from accumulated .elpi files

Status: Open.

#1079 In LPCIC/coq-elpi;

· yoshihiro503 opened on Jul 29, 2026

typecheck error

Status: Open.

#1068 In LPCIC/coq-elpi;

· Craither opened on Jul 10, 2026

The strong induction principle fails to be generated for an inductive type with nested containers

Status: Open.

#1066 In LPCIC/coq-elpi;

· StevenSharker opened on Jul 10, 2026

🐛 Cannot install coq-elpi 3.2.0 with Coq 8.20: elpi_plugin.cmxs: No such file or directory

Status: Open.

#1061 In LPCIC/coq-elpi;

· yoshihiro503 opened on Jul 2, 2026

Transitive accumulate not reflected in Extra Dependency -> rocq dep

Status: Open.

#1037 In LPCIC/coq-elpi;

· gares opened on Jun 9, 2026

Avoid contaminating clients with Set Uniform Inductive Parameters

Status: Open.

#1034 In LPCIC/coq-elpi;

· rlepigre-skylabs-ai opened on Jun 5, 2026

Elpi Accumulate can still accumulate the same file two times.

Status: Open.

#1029 In LPCIC/coq-elpi;

· MysaaJava opened on May 28, 2026

Anomaly when using HB.instance and shadowing a variable in the context

Status: Open.

#1020 In LPCIC/coq-elpi;

· sarranz opened on May 13, 2026

discriminate depends on derive.bcongr and derive.eqK for a wrong reason

Status: Open.

#1016 In LPCIC/coq-elpi;

· Tvallejos opened on May 11, 2026

Elpi databases should be subject to substitution when module types are involved

Status: Open.

#989 In LPCIC/coq-elpi;

· JasonGross opened on Mar 31, 2026

Glob: References of notation by #[short ..] attribute is incorrect

Status: Open.

#981 In LPCIC/coq-elpi;

· yoshihiro503 opened on Mar 18, 2026

Undeclared universe error when passing two ctx-decl arguments

Status: Open.

#972 In LPCIC/coq-elpi;

· VojtechStep opened on Mar 9, 2026