Search results

Checking evar candidates against some rhs forgets constraints

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

kind: internalAPI, ML documentation...API, ML documentation...

Status: Open.

#22126 In rocq-prover/rocq;

· yannl35133 opened on Jun 13, 2026

lia (zify) fails to recognize large nat literals

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

kind: enhancementEnhancement to an existing user-facing feature, tactic, etc.Enhancement to an existing user-facing feature, tactic, etc.

part: micromegaThe lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.

Status: Open.

#22122 In rocq-prover/rocq;

· JasonGross opened on Jun 11, 2026

Pattern-matching emulation for primitive record weakens typability

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

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

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.

Status: Open.

#22110 In rocq-prover/rocq;

· ppedrot opened on Jun 10, 2026

[Feature] Ltac2 error kind that escapes typeclass resolution but is still catchable

kind: enhancementEnhancement to an existing user-facing feature, tactic, etc.Enhancement to an existing user-facing feature, tactic, etc.

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

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

part: typeclassesThe typeclass mechanism.The typeclass mechanism.

Status: Open.

#22101 In rocq-prover/rocq;

· JasonGross opened on Jun 6, 2026

Search modulo Casing

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

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.

Status: Open.

#22100 In rocq-prover/rocq;

· thomas-lamiaux opened on Jun 5, 2026

Inference of canonical instances on fun ... => key ... does not always work

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.

Status: Open.

#22095 In rocq-prover/rocq;

· pi8027 opened on Jun 4, 2026

Evolution of performance

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

kind: regressionProblems that were not present in previous versions.Problems that were not present in previous versions.

Status: Open.

#22094 In rocq-prover/rocq;

· silene opened on Jun 4, 2026

Documentation on opaque module type ascription is lacking

kind: documentationAdditions or improvement to documentation.Additions or improvement to documentation.

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

Status: Open.

#22082 In rocq-prover/rocq;

· JasonGross opened on May 29, 2026

refine unshelves previously shelved evars

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.

Status: Open.

#22076 In rocq-prover/rocq;

· Janno opened on May 28, 2026

Evar unified/restricted too eagerly when arguments are Axioms

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.

Status: Open.

#22067 In rocq-prover/rocq;

· Janno opened on May 26, 2026

confused automatic level handling in custom notation starting with ident

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

part: notationsThe notation system.The notation system.

Status: Open.

#22063 In rocq-prover/rocq;

· SkySkimmer opened on May 23, 2026

ssr apply: called through user tactic notation clears the wrong variable

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

part: ssreflectThe SSReflect proof language.The SSReflect proof language.

Status: Open.

#22057 In rocq-prover/rocq;

· SkySkimmer opened on May 23, 2026