Search results

TC solver introduces eta-expansions and fails

Status: Open.

#952 In LPCIC/coq-elpi;

· Tragicus opened on Jan 21, 2026

Make <code>coq.env.section</code> return section definitions like <code>coq.env.module</code> does

Status: Open.

#950 In LPCIC/coq-elpi;

· FrogOfJuly opened on Jan 14, 2026

Anomaly with universe variables

Status: Open.

#944 In LPCIC/coq-elpi;

· patrick-nicodemus opened on Dec 15, 2025

mk-app can produce ill-formed terms

Status: Open.

#941 In LPCIC/coq-elpi;

· MysaaJava opened on Dec 13, 2025

Fatal errors in Elpi tactic can be caught by tactic-in-term

Status: Open.

#935 In LPCIC/coq-elpi;

· pi8027 opened on Nov 25, 2025

[NES] export/include namespaces

Status: Open.

#931 In LPCIC/coq-elpi;

· pi8027 opened on Nov 20, 2025

coq.elaborate-skeleton abstracts over evars

Status: Open.

#919 In LPCIC/coq-elpi;

· Tragicus opened on Oct 28, 2025

change with

Status: Open.

#917 In LPCIC/coq-elpi;

· patrick-nicodemus opened on Oct 25, 2025

naming of coq.build-match

Status: Open.

#916 In LPCIC/coq-elpi;

· patrick-nicodemus opened on Oct 25, 2025

Documentation of set-goal-arguments

Status: Open.

#914 In LPCIC/coq-elpi;

· patrick-nicodemus opened on Oct 21, 2025

ltac1 bridge is sensitive to <code>name</code>?

Status: Open.

#912 In LPCIC/coq-elpi;

· patrick-nicodemus opened on Oct 19, 2025

Anomaly in parsing inputs

Status: Open.

#910 In LPCIC/coq-elpi;

· patrick-nicodemus opened on Oct 18, 2025