-
Notifications
You must be signed in to change notification settings - Fork 741
All issues
Issue creation is restricted in this repository
- #20546 · RuifengFu opened
on Apr 19, 2025 11
Issues
is:issue state:open
is:issue state:open
Search results
Compilation of critical bugs in stable releases of Coq: add a table
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.#22301 In rocq-prover/rocq;Universe checking state gets confused when locally changed in module
kind: inconsistencyProof of False accepted by the kernel and/or checker.Proof of False accepted by the kernel and/or checker.part: modulesThe module system of Coq.The module system of Coq.part: universesThe universe system.The universe system.Status: Open.#22287 In rocq-prover/rocq;Chaining module
<+operator shows quadratic time increasekind: performanceImprovements to performance and efficiency.Improvements to performance and efficiency.part: modulesThe module system of Coq.The module system of Coq.Status: Open.#22279 In rocq-prover/rocq;Rewrite fails to rewrite a list of functions while setoid_rewrite succeeds
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.#22269 In rocq-prover/rocq;(Separate) Extraction should use "Rocq" as prefix rather than "Coq"
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.#22229 In rocq-prover/rocq;- Status: Open.#22227 In rocq-prover/rocq;
Autogeneration of transitivity lemma preempts setoid even when it fails
kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.Status: Open.#22224 In rocq-prover/rocq;Record
withsyntax that forces the record valuekind: wishFeature or enhancement requests.Feature or enhancement requests.Status: Open.#22222 In rocq-prover/rocq;Preterm construction should be referentially transparent
kind: bugAn error, flaw, fault or unintended behaviour.An error, flaw, fault or unintended behaviour.kind: wishFeature or enhancement requests.Feature or enhancement requests.part: elaborationThe elaboration engine, also known as the pretyper.The elaboration engine, also known as the pretyper.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.#22219 In rocq-prover/rocq;"Closed notations should usually be at level 0" but not always
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.#22215 In rocq-prover/rocq;Various tactics do not work on sort-polymorphic goal.
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.#22212 In rocq-prover/rocq;- Status: Open.#22191 In rocq-prover/rocq;