Search results

Anomaly "intern function not found: equations_list."

Status: Open.

#713 In rocq-prover/equations;

· fpottier opened on Apr 21, 2026

Using Equations yields 75x slowdown compared with structural recursion

Status: Open.

#710 In rocq-prover/equations;

· fpottier opened on Apr 9, 2026

Extensionality Tactic does not seem to be running the Obligation Tactic as implied by error message

Status: Open.

#708 In rocq-prover/equations;

· Durbatuluk1701 opened on Mar 26, 2026

No package compatible with rocq 9.2.dev

Status: Open.

#693 In rocq-prover/equations;

· RalfJung opened on Jan 23, 2026

funelim of high order function using Type results in "Product do not match" error

Status: Open.

#660 In rocq-prover/equations;

· terencode opened on Jul 26, 2025

Vernacular Derive conflicts with Rocq Derive feature

Status: Open.

#656 In rocq-prover/equations;

· andres-erbsen opened on Jun 14, 2025

Missing equality hypothesis in proof obligation?

Status: Open.

#654 In rocq-prover/equations;

· fpottier opened on May 9, 2025

Equations does not handle implicit constructor coercions in patterns

Status: Open.

#647 In rocq-prover/equations;

· tperami opened on Apr 9, 2025

Bug in graph generation causes illegal application

Status: Open.

#643 In rocq-prover/equations;

· joscoh opened on Mar 24, 2025

Improve deplim etc...

Status: Open.

#638 In rocq-prover/equations;

· thomas-lamiaux opened on Feb 18, 2025

Regression with Coq 8.20: ill-typed term with universe issue

Status: Open.

#635 In rocq-prover/equations;

· Armael opened on Jan 30, 2025

Ill-typed term produced after name collision (?)

Status: Open.

#634 In rocq-prover/equations;

· Armael opened on Jan 30, 2025