Issues

• SN failure due to issue in guard checking reduction

  kind: bugpart: fixpoints
  rocq-prover/rocq#22572 · Filter by author thomas-lamiaux opened on Oct 8, 2026
  2

• With -norec, rocq check prints instantiated Module Type parameters as Axioms?

  kind: bugneeds: triage
  rocq-prover/rocq#22569 · Filter by author andres-erbsen opened on Oct 8, 2026

• Qed fails using vm_compute and native_compute on inductive with let in constructors

  kind: bugneeds: triage
  rocq-prover/rocq#22568 · Filter by author yforster opened on Oct 7, 2026
  4

• Silent flag cannot be switched off

  kind: bugneeds: triage
  rocq-prover/rocq#22557 · Filter by author lweqx opened on Oct 4, 2026
  2

• Primitive operation with name alias not working with cbn

  kind: bugneeds: triage
  rocq-prover/rocq#22550 · Filter by author clarus opened on Oct 1, 2026

• Scope annotations %scope in terms shouldn't close shallow scope opening

  kind: bugneeds: triage
  rocq-prover/rocq#22547 · Filter by author proux01 opened on Oct 1, 2026

• Rocqide should have rocq-core as a dependency

  kind: wishneeds: triage
  rocq-prover/rocq#22543 · Filter by author Mbodin opened on Oct 1, 2026

• Anomaly during inductive subtyping check

  kind: anomalypart: inductivespart: modules
  rocq-prover/rocq#22498 · Filter by author yannl35133 opened on Sep 17, 2026
  1

• Only-printing notation changes precedence of a later parsing rule

  kind: bugneeds: triage
  rocq-prover/rocq#22496 · Filter by author remix7531 opened on Sep 17, 2026
  1

• Assertion failure in mod_subst

  kind: anomalypart: modules
  rocq-prover/rocq#22482 · Filter by author ppedrot opened on Sep 16, 2026
  1

• RocqIDE external command defaults still use compatibility Coq binaries

  rocq-prover/rocq#22473 · Filter by author zhaob1n opened on Sep 12, 2026
  2

• Primitive operations in the VM do not work well with module aliasing

  part: modulespart: VM
  rocq-prover/rocq#22470 · Filter by author ppedrot opened on Sep 10, 2026

• timelog2html incorrectly considers preceding character as part of a command

  kind: bug
  rocq-prover/rocq#22467 · Filter by author SkySkimmer opened on Sep 10, 2026

• Register Inline is not saved to the .vo, so it has no effect in files that Require the defining one

  rocq-prover/rocq#22460 · Filter by author JasonGross opened on Sep 9, 2026

• Clarify extraction correctness for strict let-bindings and exception-raising external functions

  rocq-prover/rocq#22450 · Filter by author JiaJunDeng5930 opened on Sep 9, 2026
  3

• Anomaly "Missing VM index" when vm_compute reaches a constant of a module sealed with "with Definition"

  rocq-prover/rocq#22449 · Filter by author JasonGross opened on Sep 8, 2026

• Anomaly "Uncaught exception Failure("List.chop")." when parsing notation.

  kind: bugneeds: triage
  rocq-prover/rocq#22448 · Filter by author Remyjck opened on Sep 8, 2026

• Add an option for per-file lia caching

  kind: performancekind: wishpart: micromega
  rocq-prover/rocq#22440 · Filter by author JasonGross opened on Sep 4, 2026

• What would it take for a Vernacstate.t to be transportable between directories or machines?

  rocq-prover/rocq#22432 · Filter by author remix7531 opened on Sep 1, 2026
  2

• -async-proofs on: coqc exits 0 and writes a consumable .vo for an ill-typed file

  kind: bugpart: STM
  rocq-prover/rocq#22422 · Filter by author JasonGross opened on Aug 29, 2026

• Large inclusion of modules is slow due to Libobject expansion

  kind: performancepart: libobjectpart: modules
  rocq-prover/rocq#22420 · Filter by author ppedrot opened on Aug 29, 2026

• Anomaly Bad occurrence of recursive call. (with fix tactic)

  kind: anomalypart: fixpoints
  rocq-prover/rocq#22417 · Filter by author yannl35133 opened on Aug 28, 2026

• Bug in = mode, or the mode is less useful than expected

  kind: bugneeds: triage
  rocq-prover/rocq#22414 · Filter by author robbertkrebbers opened on Aug 28, 2026
  17

• RocqIDE executes attacker code on file open by applying an ancestor-directory _RocqProject that injects -l into the coqidetop argv

  rocq-prover/rocq#22406 · Filter by author ppedrot opened on Aug 26, 2026

• Unvalidated bytecode operand counts in rocq_tcode_of_code cause an attacker-length heap buffer overflow when loading a crafted .vo

  kind: kernel segfault/exploit
  rocq-prover/rocq#22405 · Filter by author ppedrot opened on Aug 26, 2026
  4