rocq-prover

Las issues en las que quizá ya trabaja alguien aparecen al final. Ordenar todo por fecha

• `Silent` flag cannot be switched off

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug needs: triage

  Dificultad 3/5 Medio día Aptitud para principiantes 62/100

  rocq-prover/rocq#22557 · Abierto el 4/10/2026

  Los mantenedores suelen responder en 1 día

• Please add "rocq-equations.1.3.2+9.3" to the `released` opam archive.

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 1/5 Menos de una hora Aptitud para principiantes 68/100

  rocq-prover/equations#745 · Abierto el 4/10/2026

• Primitive operation with name alias not working with cbn

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug needs: triage

  Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

  rocq-prover/rocq#22550 · Abierto el 1/10/2026

  Los mantenedores suelen responder en 1 día

• Print Assumptions lists an implemented interface as so many axioms

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug needs: triage part: modules

  Dificultad 3/5 1-2 días Aptitud para principiantes 58/100

  rocq-prover/rocq#22533 · 1 comentario · Abierto el 25/9/2026

  Los mantenedores suelen responder en 1 día

• dangling pointer to "who did what"

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 2/5 1-3 horas Aptitud para principiantes 65/100

  rocq-prover/rocq-prover.org#273 · Abierto el 25/9/2026

• [BUG] Stack overflow kills the language server instead of reporting an error (macOS)

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  rocq-prover/vsrocq#1331 · 3 comentarios · Abierto el 25/9/2026

  Los mantenedores suelen responder en 1 día

• [BUG] Messages panel not clearing out previous Info messages on edit

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  bug

  Dificultad 3/5 1-2 días Aptitud para principiantes 62/100

  rocq-prover/vsrocq#1328 · 1 reacción · Abierto el 24/9/2026

  Los mantenedores suelen responder en 1 día

• Difference to fixpoints in catch-all/default branches leading to guard checker problems

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  rocq-prover/equations#742 · Abierto el 18/9/2026

• Anomaly during inductive subtyping check

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: anomaly part: inductives part: modules

  Dificultad 4/5 3-5 días Aptitud para principiantes 30/100

  rocq-prover/rocq#22498 · 1 comentario · Abierto el 17/9/2026

  Los mantenedores suelen responder en 1 día

• Specify that Intel Macs require installing from source

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 1/5 Menos de una hora Aptitud para principiantes 90/100

  rocq-prover/platform#537 · 1 comentario · 1 reacción · Abierto el 16/9/2026

• Assertion failure in mod_subst

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: anomaly part: modules

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  rocq-prover/rocq#22482 · 1 comentario · Abierto el 16/9/2026

  Los mantenedores suelen responder en 1 día

• [FEAT] Extend `textDocument/selectionRange` to be AST aware

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  enhancement

  Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

  rocq-prover/vsrocq#1323 · 1 comentario · Abierto el 16/9/2026

  Los mantenedores suelen responder en 1 día

• documentation of install buildtools for Fedora

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 1/5 Menos de una hora Aptitud para principiantes 92/100

  rocq-prover/platform#536 · 1 comentario · 1 reacción · Abierto el 14/9/2026

• RocqIDE external command defaults still use compatibility Coq binaries

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 2/5 1-3 horas Aptitud para principiantes 76/100

  rocq-prover/rocq#22473 · 2 comentarios · Abierto el 12/9/2026

  Los mantenedores suelen responder en 1 día

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

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  part: modules part: VM

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  rocq-prover/rocq#22470 · Abierto el 10/9/2026

  Los mantenedores suelen responder en 1 día

• timelog2html incorrectly considers preceding character as part of a command

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug

  Dificultad 3/5 1-2 días Aptitud para principiantes 65/100

  rocq-prover/rocq#22467 · Abierto el 10/9/2026

  Los mantenedores suelen responder en 1 día

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

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 65/100

  rocq-prover/rocq#22460 · Abierto el 9/9/2026

  Los mantenedores suelen responder en 1 día

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

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  rocq-prover/rocq#22450 · 3 comentarios · 1 reacción · Abierto el 9/9/2026

  Los mantenedores suelen responder en 1 día

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

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 58/100

  rocq-prover/rocq#22449 · Abierto el 8/9/2026

  Los mantenedores suelen responder en 1 día

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

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug needs: triage

  Dificultad 4/5 3-5 días Aptitud para principiantes 55/100

  rocq-prover/rocq#22448 · Abierto el 8/9/2026

  Los mantenedores suelen responder en 1 día

• Add an option for per-file lia caching

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: performance kind: wish part: micromega

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  rocq-prover/rocq#22440 · Abierto el 4/9/2026

  Los mantenedores suelen responder en 1 día

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

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 30/100

  rocq-prover/rocq#22432 · 2 comentarios · Abierto el 1/9/2026

  Los mantenedores suelen responder en 1 día

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

  Quizá libre de nuevo Un pull request para esta issue se cerró sin fusionarse. Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug part: STM

  Dificultad 3/5 1-2 días Aptitud para principiantes 35/100

  rocq-prover/rocq#22422 · Abierto el 29/8/2026

  Los mantenedores suelen responder en 1 día

• Large inclusion of modules is slow due to Libobject expansion

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: performance part: libobject part: modules

  Dificultad 4/5 3-5 días Aptitud para principiantes 42/100

  rocq-prover/rocq#22420 · Abierto el 29/8/2026

  Los mantenedores suelen responder en 1 día

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

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: anomaly part: fixpoints

  Dificultad 3/5 1-2 días Aptitud para principiantes 65/100

  rocq-prover/rocq#22417 · Abierto el 28/8/2026

  Los mantenedores suelen responder en 1 día

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

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug needs: triage

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  rocq-prover/rocq#22414 · 17 comentarios · Abierto el 28/8/2026

  Los mantenedores suelen responder en 1 día

• Explicit argument is being shadowed by implicit argument

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 3/5 1-2 días Aptitud para principiantes 55/100

  rocq-prover/equations#741 · Abierto el 27/8/2026

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

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  rocq-prover/rocq#22406 · Abierto el 26/8/2026

  Los mantenedores suelen responder en 1 día

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

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: kernel segfault/exploit

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  rocq-prover/rocq#22405 · 4 comentarios · Abierto el 26/8/2026

  Los mantenedores suelen responder en 1 día

• About the kernel's data structures for renamings and substitutions

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: wish needs: triage

  Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

  rocq-prover/rocq#22403 · 2 comentarios · Abierto el 25/8/2026

  Los mantenedores suelen responder en 1 día

• Unexpected Behavior from `rewrite_strat` when moving terms in and out of binders

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug needs: triage

  Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

  rocq-prover/rocq#22397 · Abierto el 21/8/2026

  Los mantenedores suelen responder en 1 día

• `-async-proofs on` silently swallows universe-constraint errors (exit 0, `.vo` silently missing the failed definition)

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug needs: triage

  Dificultad 4/5 3-5 días Aptitud para principiantes 52/100

  rocq-prover/rocq#22367 · Abierto el 19/8/2026

  Los mantenedores suelen responder en 1 día

• `Unset Guard Checking` leaks through functor application with `Parameter Inline`: `False` accepted with `Print Assumptions` reporting "Closed under the global context"

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug

  Dificultad 5/5 Más de una semana Aptitud para principiantes 32/100

  rocq-prover/rocq#22366 · 1 comentario · Abierto el 19/8/2026

  Los mantenedores suelen responder en 1 día

• Nested Eliminators

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: wish needs: triage

  Dificultad 5/5 Más de una semana Aptitud para principiantes 45/100

  rocq-prover/rocq#22344 · 1 reacción · Abierto el 12/8/2026

  Los mantenedores suelen responder en 1 día

• Cannot scroll on sidebar

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 3/5 1-2 días Aptitud para principiantes 58/100

  rocq-prover/rocq-prover.org#268 · Abierto el 12/8/2026

• When universes are printed, cannot accept the print of an inductive

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug needs: triage part: printer

  Dificultad 3/5 1-2 días Aptitud para principiantes 48/100

  rocq-prover/rocq#22343 · Abierto el 11/8/2026

  Los mantenedores suelen responder en 1 día

• Module ascription rejected when a component's type names a sibling module directly instead of through its alias

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: question part: modules

  Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

  rocq-prover/rocq#22333 · 1 comentario · Abierto el 6/8/2026

  Los mantenedores suelen responder en 1 día

• Anomaly unknown level with ltac2 notation

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug part: ltac2

  Dificultad 3/5 1-2 días Aptitud para principiantes 50/100

  rocq-prover/rocq#22330 · Abierto el 3/8/2026

  Los mantenedores suelen responder en 1 día

• Bidirectional hints change program obligation order in unexpected ways

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug needs: triage

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  rocq-prover/rocq#22328 · Abierto el 31/7/2026

  Los mantenedores suelen responder en 1 día

• (auto)rewrite* fails where (auto)rewrite succeeds

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug needs: triage

  Dificultad 4/5 3-5 días Aptitud para principiantes 48/100

  rocq-prover/rocq#22323 · 4 comentarios · Abierto el 29/7/2026

  Los mantenedores suelen responder en 1 día

• [release] for Rocq 9.3.0

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 25/100

  rocq-prover/vsrocq#1291 · 2 comentarios · Abierto el 28/7/2026

  Los mantenedores suelen responder en 1 día

• `vsrocq-language-server` installation fails on OCaml 5.5

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 3/5 1-2 días Aptitud para principiantes 55/100

  rocq-prover/vsrocq#1287 · 2 comentarios · Abierto el 24/7/2026

  Los mantenedores suelen responder en 1 día

• Compilation of critical bugs in stable releases of Coq: add a table

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: wish needs: triage

  Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100

  rocq-prover/rocq#22301 · 1 comentario · Abierto el 23/7/2026

  Los mantenedores suelen responder en 1 día

• Remove "vsrocq.proof.delegation"

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 2/5 1-3 horas Aptitud para principiantes 64/100

  rocq-prover/vsrocq#1286 · 1 comentario · Abierto el 21/7/2026

  Los mantenedores suelen responder en 1 día

• The link in repo description is invalid

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100

  rocq-prover/equations#731 · Abierto el 21/7/2026

• Universe checking state gets confused when locally changed in module

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: inconsistency part: modules part: universes

  Dificultad 3/5 1-2 días Aptitud para principiantes 48/100

  rocq-prover/rocq#22287 · Abierto el 16/7/2026

  Los mantenedores suelen responder en 1 día

• Chaining module `<+` operator shows quadratic time increase

  Quizá libre de nuevo Un pull request para esta issue se cerró sin fusionarse. Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: performance part: modules

  Dificultad 4/5 3-5 días Aptitud para principiantes 42/100

  rocq-prover/rocq#22279 · 3 comentarios · Abierto el 16/7/2026

  Los mantenedores suelen responder en 1 día

• Maintaining NaryFunctions

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100

  rocq-prover/stdlib#293 · Abierto el 15/7/2026

• Rewrite fails to rewrite a list of functions while setoid_rewrite succeeds

  Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar
  kind: bug needs: triage

  Dificultad 4/5 3-5 días Aptitud para principiantes 42/100

  rocq-prover/rocq#22269 · 2 comentarios · Abierto el 12/7/2026

  Los mantenedores suelen responder en 1 día

• Typeclass resolution regression from #22037: goals with no applicable hint fail eagerly, losing solutions found via later unifications (breaks fiat-crypto)

  Quizá libre de nuevo Un pull request para esta issue se cerró sin fusionarse. Abierto

  ⋯Informar de un problema con este issue

  • ¿Algo no está bien?

  • Ya está asignado
  • No es para principiantes
  • Obsoleto o no válido
  • Otra cosa…
  • Enviar Cancelar

  Dificultad 4/5 3-5 días Aptitud para principiantes 45/100

  rocq-prover/rocq#22227 · 2 comentarios · Abierto el 7/7/2026

  Los mantenedores suelen responder en 1 día