Skip to content

Issues: coq/coq

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

2,513 Open 7,558 Closed
2,513 Open 7,558 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Notation using pattern matching on booleans is only parsing kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Error messages, warnings, etc. part: notations The notation system.
#20068 opened Jan 16, 2025 by amblafont
2
Anomaly on parsing string notations generated by Include. kind: bug An error, flaw, fault or unintended behaviour.
#20067 opened Jan 16, 2025 by gmalecha
1
Replace Coq icons with Rocq Prover ones in sources priority: blocker The next release should be delayed if this is not fixed.
#20059 opened Jan 15, 2025 by Zimmi48 9.0+rc1
Params instances are not used for setoid_rewrite with types kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#20044 opened Jan 14, 2025 by quarkcool
1
Allow error messages from string notation parsers kind: wish Feature or enhancement requests. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#20042 opened Jan 13, 2025 by gmalecha
"Anomaly in Univ.repr" : when using a lemma in a program definition kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#20033 opened Jan 13, 2025 by forrazh
"Dependent induction is not allowed for inductive definition" should describe why dependent induction is not allowed kind: user messages Error messages, warnings, etc. kind: wish Feature or enhancement requests.
#20032 opened Jan 12, 2025 by JasonGross
2
opam pin add coq --dev-repo no longer works kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#20030 opened Jan 12, 2025 by JasonGross
Bad case inversion with Set Definitional UIP kind: bug An error, flaw, fault or unintended behaviour. part: SProp Proof irrelevance and strict propositions.
#20016 opened Jan 10, 2025 by ppedrot
5
discriminate and congruence cannot distinguish primitive values kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated. part: congruence The congruence tactic. part: tactics
#20011 opened Jan 10, 2025 by Janno
Arguments ! on primitive projection parameters should warn that it is ignored part: primitive records The primitive record and primitive projection mechanism.
#20009 opened Jan 10, 2025 by SkySkimmer
1
Failing view when "apply ... in" succeeds kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#19999 opened Jan 9, 2025 by amahboubi
Anomaly "Uncaught exception Not_found." when destructing an inductive type as a resolvable opaque reference kind: anomaly An uncaught exception has been raised. kind: bug An error, flaw, fault or unintended behaviour.
#19994 opened Jan 8, 2025 by radrow
1
coqnative anomaly on complicated fixpoint generated by Equations kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#19986 opened Jan 6, 2025 by jpoiret
1
Module constraints involving functors are not handled properly in the upper layers kind: bug An error, flaw, fault or unintended behaviour. part: modules The module system of Coq.
#19984 opened Jan 6, 2025 by ppedrot
The problem when doing a case analysis on a type based on a private type (but not private itself.) kind: bug An error, flaw, fault or unintended behaviour. part: inductives Inductive types, fixpoints, etc. part: pattern-matching compilation
#19983 opened Jan 6, 2025 by sehun1024
Change the theme of the refman and the stdlib priority: blocker The next release should be delayed if this is not fixed.
#19976 opened Dec 26, 2024 by Zimmi48 9.0+rc1
@mattam82
5
Release 9.0
#19974 opened Dec 24, 2024 by ppedrot
15 of 40 tasks
Anomaly "File "kernel/indTyping.ml", line 345, characters 17-23: Assertion failed." with forced template on incorrect syntax kind: anomaly An uncaught exception has been raised.
#19971 opened Dec 20, 2024 by SkySkimmer
coqorg/coq:dev build is broken since yesterday: ideas to improve the process? kind: meta About the process of developing Coq.
#19962 opened Dec 19, 2024 by erikmd
2
extensionality tactic is missing in the manual kind: bug An error, flaw, fault or unintended behaviour. kind: documentation Additions or improvement to documentation.
#19948 opened Dec 17, 2024 by yaitskov
1
Inaccurate tactic trace from Set Typeclasses Debug kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Error messages, warnings, etc. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#19930 opened Dec 13, 2024 by JonasOberhauser
Lia fails to prove (Z.to_nat 1) = 1%nat if a proof for this goal already exists as record member in the context. kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated. part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.
#19924 opened Dec 12, 2024 by MSoegtropIMC
1
Inconsistent behaviour between Program Definition and Program Definition :=. kind: wish Feature or enhancement requests. part: program
#19922 opened Dec 11, 2024 by CohenCyril
1
"Obligation Tactic" is global, causing trouble when two libraries want to control it
#19902 opened Dec 5, 2024 by RalfJung
1
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.