Search results

<code>Proof</code> command is not always a no-op.

Status: Open.

#20936 In rocq-prover/rocq;

· upamanyus opened on Jul 18, 2025

Warning: Tolerating this expression at level &lt;unknown&gt; while it is expected to be at level &lt;unknown&gt;.

Status: Open.

#20932 In rocq-prover/rocq;

· SkySkimmer opened on Jul 18, 2025

Anomaly "Uncaught exception Option.IsNone."

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

part: ltac debuggerIssues and PRs related to the Ltac debugger, visual CoqIDE debugger etc.Issues and PRs related to the Ltac debugger, visual CoqIDE debugger etc.

Status: Open.

#20930 In rocq-prover/rocq;

· lunakoly opened on Jul 18, 2025

listing opam package dependencies of files

kind: infrastructureCI, build tools, development tools.CI, build tools, development tools.

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

Status: Open.

#20929 In rocq-prover/rocq;

· JasonGross opened on Jul 17, 2025

Rocq 9.0.0: Error: not found in table: core.JMeq.type

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.

#20927 In rocq-prover/rocq;

· Flupp opened on Jul 17, 2025

Empty code div at the beginning of some corelib doc files looks bad

Status: Open.

#20922 In rocq-prover/rocq;

· SkySkimmer opened on Jul 17, 2025

coqchk broken on global sorts (missing values update)

part: checkerThe coqchk binary for validating .vo files.The coqchk binary for validating .vo files.

Status: Open.

#20920 In rocq-prover/rocq;

· SkySkimmer opened on Jul 17, 2025

Anomaly (Assertion failed) in <code>clearbody</code> inside <code>match</code>

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

Status: Open.

#20919 In rocq-prover/rocq;

· yanjs opened on Jul 17, 2025

Consistent-ecosystem pickup of 9.0

kind: design discussionDiscussion about the design of a feature.Discussion about the design of a feature.

Status: Open.

#20918 In rocq-prover/rocq;

· andres-erbsen opened on Jul 16, 2025

derive should name goals

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

Status: Open.

#20915 In rocq-prover/rocq;

· SkySkimmer opened on Jul 16, 2025

About on abbreviation should mention argument scopes

kind: user messagesError messages, warnings, etc.Error messages, warnings, etc.

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

Status: Open.

#20899 In rocq-prover/rocq;

· SkySkimmer opened on Jul 10, 2025

Build system documentation is incorrect after #20881

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

kind: infrastructureCI, build tools, development tools.CI, build tools, development tools.

part: buildThe build system.The build system.

Status: Open.

#20895 In rocq-prover/rocq;

· ejgallego opened on Jul 10, 2025