-
Notifications
You must be signed in to change notification settings - Fork 755
OpenAug 27, 2026
No due date
•Last updated @coqbot: backport to v9.2 (move rejected PRs to: https://github.com/coq/coq/milestone/69); backport to v9.3 (move rejected PRs to: https://github.com/coq/coq/milestone/73)
91% complete
List view
0 of 5 selected 0 issues of 5 selected
Make Nativecode.string_of_kn really injective for good.
kind: fixThis fixes a bug or incorrect documentation.This fixes a bug or incorrect documentation.kind: inconsistencyProof of False accepted by the kernel and/or checker.Proof of False accepted by the kernel and/or checker.Status: Open (in progress).Do not trust the serialized VM bytecode in rocqchk
kind: inconsistencyProof of False accepted by the kernel and/or checker.Proof of False accepted by the kernel and/or checker.part: checkerThe coqchk binary for validating .vo files.The coqchk binary for validating .vo files.Status: Open (in progress).Correctly validate block tags in rocqchk demarshaller.
kind: fixThis fixes a bug or incorrect documentation.This fixes a bug or incorrect documentation.Status: Open (in progress).Only count uniform arguments that correponds to lambdas
kind: fixThis fixes a bug or incorrect documentation.This fixes a bug or incorrect documentation.part: inductivesInductive types, fixpoints, etc.Inductive types, fixpoints, etc.Status: Open (in progress).Name confusion in δ-resolver inclusion leading to an inconsistency
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.Status: Open.#22409 In rocq-prover/rocq;