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,549 Open 7,507 Closed
2,549 Open 7,507 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

"About" shows wrong implicits after Require Import Utf8 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.
#19702 opened Oct 16, 2024 by eponier
-time changes the timing 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.
#19689 opened Oct 14, 2024 by Tragicus
10
Hint Resolve registers the same hint for a definitional class multiple times at different patterns 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: typeclasses The typeclass mechanism.
#19681 opened Oct 12, 2024 by Janno
9
"Bind Scope" does not for already-defined notations
#19676 opened Oct 11, 2024 by RalfJung
9
Feature request: provide a way to do notypeclasses refine while honoring opacity hints kind: wish Feature or enhancement requests. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#19666 opened Oct 9, 2024 by RalfJung
Unexpected warning about incompatible notation kind: bug An error, flaw, fault or unintended behaviour. part: notations The notation system.
#19658 opened Oct 8, 2024 by RalfJung 8.20.1
1
1
"Uncaught exception Not_found." when trying to rewrite 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.
#19651 opened Oct 7, 2024 by JulesViennotFranca
Taking a long time to type check inductive types
#19650 opened Oct 7, 2024 by JulesViennotFranca
6
discriminate and injection do not work with sort polymorphic inductive 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.
#19637 opened Oct 3, 2024 by tabareau
1
Extraction produces a malformed recursive function definition with no argument kind: bug An error, flaw, fault or unintended behaviour. part: extraction The extraction mechanism.
#19636 opened Oct 3, 2024 by PierreCorbineau
Extraction fails with anomaly for second mutually defined fixpoint kind: bug An error, flaw, fault or unintended behaviour. part: extraction The extraction mechanism.
#19635 opened Oct 3, 2024 by PierreCorbineau
Variant of discriminate that refutes statements such as "S n <= 0" kind: wish Feature or enhancement requests. part: inversion tactics The injection, discriminate, inversion tactics
#19633 opened Oct 3, 2024 by herbelin
3
Spurious "incompatible prefixes" warning for "printing only" notations kind: bug An error, flaw, fault or unintended behaviour. part: notations The notation system.
#19631 opened Oct 2, 2024 by robbertkrebbers 8.20.1
2
Rewrite Rules and constant functions kind: wish Feature or enhancement requests. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#19608 opened Sep 25, 2024 by soundlogic2236
"From Coq Require Import XYZ" error message refers to Stdlib kind: usability Not a bug (fix) but a usability issue / improvement, e.g. UI or syntax inconsistencies kind: user messages Improvement of error messages, new warnings, etc. part: CoqIDE Issues and PRs related to CoqIDE or other IDE features of coq.
#19606 opened Sep 25, 2024 by jfehrle
6
#[universes(template)] fails when univ poly is set
#19604 opened Sep 25, 2024 by SkySkimmer
coqc -beautify also generates ~/.coqrc.beautified kind: bug An error, flaw, fault or unintended behaviour.
#19603 opened Sep 25, 2024 by SkySkimmer
Print Current Proof State when a Command or Tactic Fails kind: wish Feature or enhancement requests. part: compiler
#19601 opened Sep 24, 2024 by gmalecha
8
Naming intropattern is not respected (with apply in) kind: bug An error, flaw, fault or unintended behaviour.
#19600 opened Sep 24, 2024 by MevenBertrand
SSReflect => > breaks with forall X, X (uncaught Not_found) kind: bug An error, flaw, fault or unintended behaviour. part: ssreflect The SSReflect proof language.
#19598 opened Sep 23, 2024 by yannl35133
Fixpoint inside a lemma produces anomaly universe undefined kind: bug An error, flaw, fault or unintended behaviour.
#19593 opened Sep 22, 2024 by svyatlovskiy
1
3
Rewrite rules under eta kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: rewrite rules
#19592 opened Sep 22, 2024 by Alizter
9
SSReflect's @ and {} don't interact correctly 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.
#19582 opened Sep 20, 2024 by yannl35133
Hint Cut in auto and eauto kind: wish Feature or enhancement requests. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#19580 opened Sep 20, 2024 by radrow
4
Changelog: autogenerate ref for each section kind: documentation Additions or improvement to documentation. kind: wish Feature or enhancement requests.
#19571 opened Sep 19, 2024 by SkySkimmer
ProTip! Adding no:label will show everything without a label.