Search results

Target ci-all fails for fiat_crypto_legacy

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.

#20886 In rocq-prover/rocq;

· dwRchyngqxs opened on Jul 8, 2025

<code>congruence</code> tactic runtime can be exponential

Status: Open.

#20884 In rocq-prover/rocq;

· upamanyus opened on Jul 8, 2025

Uncaught exception Evarsolve.IllTypedInstance

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

part: pattern-matching compilation

part: universesThe universe system.The universe system.

Status: Open.

#20875 In rocq-prover/rocq;

· doside opened on Jul 7, 2025

Conversion test raised an anomaly

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

Status: Open.

#20874 In rocq-prover/rocq;

· doside opened on Jul 7, 2025

Ltac2 eval_red should not raise uncatchable errors

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

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

Status: Open.

#20871 In rocq-prover/rocq;

· JasonGross opened on Jul 7, 2025

Loop in unification.ml with eta-rule for records

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

part: canonical structureThe Canonical Structure mechanism.The Canonical Structure mechanism.

part: unificationThe unification mechanism.The unification mechanism.

Status: Open.

#20852 In rocq-prover/rocq;

· Tragicus opened on Jul 2, 2025

retyping complains that a bound variable is unbound (Error: Anomaly "in retyping: Variable hx1 unbound." Please report at http://coq.inria.fr/bugs/.)

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: existential variablesExistential variables, also known as evars, represent as yet unknown values in a proof.Existential variables, also known as evars, represent as yet unknown values in a proof.

Status: Open.

#20851 In rocq-prover/rocq;

· JasonGross opened on Jul 2, 2025

Shadowing does not work as expected when section variables are involved

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.

#20847 In rocq-prover/rocq;

· Janno opened on Jul 1, 2025

Anomaly with modules and number notations

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.

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: modulesThe module system of Coq.The module system of Coq.

Status: Open.

#20846 In rocq-prover/rocq;

· yannl35133 opened on Jul 1, 2025

rocq dep can't find non-<code>.v</code> extra dependency specified in <code>ROCQPATH</code>

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.

#20835 In rocq-prover/rocq;

· VojtechStep opened on Jun 30, 2025

Ltac2 profiler no longer works

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

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

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

Status: Open.

#20818 In rocq-prover/rocq;

· JasonGross opened on Jun 27, 2025

Show command with diffs

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

Status: Open.

#20793 In rocq-prover/rocq;

· hendriktews opened on Jun 23, 2025