Search results

Error: Anomaly "Non-qed command classified incorrectly"

kind: anomalyAn uncaught exception has been raised.An uncaught exception has been raised.

kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.

Status: Open.

#21091 In rocq-prover/rocq;

· JasonGross opened on Sep 18, 2025

Anomaly "Uncaught exception Not_found." with local reserved notation in imported module

kind: anomalyAn uncaught exception has been raised.An uncaught exception has been raised.

kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.

part: modulesThe module system of Coq.The module system of Coq.

part: notationsThe notation system.The notation system.

Status: Open.

#21077 In rocq-prover/rocq;

· yannl35133 opened on Sep 10, 2025

Associativity issues in refman

Status: Open.

#21072 In rocq-prover/rocq;

· ia0 opened on Sep 6, 2025

Assertion failure when subtyping modules containing mutual records

Status: Open.

#21068 In rocq-prover/rocq;

· SkySkimmer opened on Sep 5, 2025

Recursive Property Bug in Function

kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.

part: funind

Status: Open.

#21064 In rocq-prover/rocq;

· barry-jay-personal opened on Sep 4, 2025

List cons is left-associative in Ltac2 patterns

kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.

Status: Open.

#21045 In rocq-prover/rocq;

· ia0 opened on Sep 2, 2025

Specifying Hint Mode(s) causes quadratic slowdown on stuck goals

kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.

needs: triageThe validity of this issue needs to be checked, or the issue itself updated.The validity of this issue needs to be checked, or the issue itself updated.

part: typeclassesThe typeclass mechanism.The typeclass mechanism.

Status: Open.

#21044 In rocq-prover/rocq;

· Janno opened on Sep 1, 2025

Using <code>-vos</code> makes fiat-crypto's critical path slower

kind: performanceImprovements to performance and efficiency.Improvements to performance and efficiency.

needs: triageThe validity of this issue needs to be checked, or the issue itself updated.The validity of this issue needs to be checked, or the issue itself updated.

part: STMState Transition Machine, asynchronous proofs, etc.State Transition Machine, asynchronous proofs, etc.

Status: Open.

#21037 In rocq-prover/rocq;

· andres-erbsen opened on Aug 29, 2025

"apply ... in" produces unbound deBruijn

kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.

Status: Open.

#21036 In rocq-prover/rocq;

· PierreCorbineau opened on Aug 27, 2025

Option to disable spontaneous goals printing

kind: wishFeature or enhancement requests.Feature or enhancement requests.

part: toplevel

Status: Open.

#21035 In rocq-prover/rocq;

· Matafou opened on Aug 27, 2025

unification is nearly impossible to debug (instantiates evars which are not mentioned in the debug trace, and the debug trace + context does not capture the relevant state)

kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.

needs: triageThe validity of this issue needs to be checked, or the issue itself updated.The validity of this issue needs to be checked, or the issue itself updated.

part: unificationThe unification mechanism.The unification mechanism.

Status: Open.

#21034 In rocq-prover/rocq;

· JasonGross opened on Aug 27, 2025

Ltac / Ltac2 escape hatch

kind: wishFeature or enhancement requests.Feature or enhancement requests.

part: ltacIssues and PRs related to the Ltac tactic language.Issues and PRs related to the Ltac tactic language.

part: ltac2Issues and PRs related to the (in development) Ltac2 tactic langauge.Issues and PRs related to the (in development) Ltac2 tactic langauge.

part: tactics

Status: Open.

#21030 In rocq-prover/rocq;

· JasonGross opened on Aug 25, 2025