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,507 Open 7,373 Closed
2,507 Open 7,373 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
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

destruct produces an ill-typed term kind: bug An error, flaw, fault or unintended behaviour.
#19004 opened May 6, 2024 by mrhaandi
1
How to report the status of existential variables in a UI in the future? kind: wish Feature or enhancement requests.
#19001 opened May 3, 2024 by hendriktews
2
Uncaught exception Failure("List.chop") in 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.
#19000 opened May 3, 2024 by JulesViennotFranca
1
Search categories for constants with opaque (lemmas, etc) and transparent (definition, ...) bodies kind: feature New user-facing feature request or implementation. kind: wish Feature or enhancement requests. part: search Search and Locate vernac commands. part: vernac High level command interpretation.
#18985 opened Apr 28, 2024 by Villetaneuse
2
commit 5c94d0d375 breaks dependent evar line kind: bug An error, flaw, fault or unintended behaviour.
#18980 opened Apr 26, 2024 by hendriktews
1
4
Unspecified universe levels (_) trigger a syntax error in Type with sort variables kind: wish Feature or enhancement requests.
#18978 opened Apr 26, 2024 by kyoDralliam
1
2
Conversion can fail to equate primitive projections with their compatibility constants kind: bug An error, flaw, fault or unintended behaviour. kind: regression Problems that were not present in previous versions. part: primitive records The primitive record and primitive projection mechanism.
#18977 opened Apr 25, 2024 by Janno
3
::> only declares an instance without a coercion when it should do both kind: bug An error, flaw, fault or unintended behaviour.
#18971 opened Apr 23, 2024 by Alizter
2
Unification ends in a stack overflow kind: bug An error, flaw, fault or unintended behaviour.
#18965 opened Apr 22, 2024 by yannl35133
1
Feature request: prepend {-# OPTIONS_GHC -w #-} to extracted Haskell files kind: wish Feature or enhancement requests. part: extraction The extraction mechanism.
#18962 opened Apr 21, 2024 by toku-sa-n
1
Qed fails on typechecking valid proof using native_compute kind: bug An error, flaw, fault or unintended behaviour. part: modules The module system of Coq. part: native compiler
#18961 opened Apr 19, 2024 by chluebi
2
Anomaly "in Lemmas.save_lemma_admitted: more than one statement." with Derive kind: anomaly An uncaught exception has been raised.
#18951 opened Apr 18, 2024 by SkySkimmer
Synterp code of creating notations unnecessarily uses notation's body kind: wish Feature or enhancement requests.
#18943 opened Apr 17, 2024 by trilis
2
Poor compilation of dependent pattern-matching in bytecode kind: performance Improvements to performance and efficiency. kind: wish Feature or enhancement requests. part: VM Virtual machine.
#18933 opened Apr 15, 2024 by silene
2
Ltac2: provide access to boxing API in printf kind: wish Feature or enhancement requests.
#18923 opened Apr 11, 2024 by MSoegtropIMC
1
Coq does not use the notation for printing (with custom entries) kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Improvement of error messages, new warnings, etc. part: notations The notation system.
#18914 opened Apr 9, 2024 by amblafont
Kernel rejects unification solution with max universes kind: bug An error, flaw, fault or unintended behaviour. part: unification The unification mechanism. part: universes The universe system.
#18904 opened Apr 5, 2024 by Janno
4
Spurious failure of SSReflect's assumption interpretation kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Improvement of error messages, new warnings, etc. part: ssreflect The SSReflect proof language.
#18898 opened Apr 5, 2024 by silene
9
More Info customization kind: user messages Improvement of error messages, new warnings, etc. kind: wish Feature or enhancement requests. part: ltac Issues and PRs related to the Ltac tactic language. part: printer The printing mechanism of Coq. part: tactics
#18889 opened Apr 3, 2024 by JasonGross
1
Release 8.20 kind: meta About the process of developing Coq.
#18882 opened Apr 2, 2024 by proux01
3 of 38 tasks
nsatz no longer unfolds TwoF kind: regression Problems that were not present in previous versions. part: nsatz The nsatz tactic
#18872 opened Mar 30, 2024 by Boutry
5
rewrite does not find seeming exact match with primitive projections kind: bug An error, flaw, fault or unintended behaviour. part: primitive records The primitive record and primitive projection mechanism. part: rewriting tactics The rewrite, autorewrite, rewrite_strat, and setoid_rewrite tactics. wellknown: unfolded primitive projections
#18871 opened Mar 30, 2024 by andres-erbsen
5
contradiction does not unify universes enough kind: bug An error, flaw, fault or unintended behaviour. part: universes The universe system. wellknown: universe polymorphism Ltac compat Turning on universe polymorphism needlessly breaks some tactic scripts
#18870 opened Mar 30, 2024 by andres-erbsen
5
Conversion incompleteness with Definitional UIP kind: bug An error, flaw, fault or unintended behaviour.
#18865 opened Mar 29, 2024 by yannl35133
1
2
destruct does not clear assumptions whose names belonged to renamed section variables difficulty: hard kind: bug An error, flaw, fault or unintended behaviour. part: ltac Issues and PRs related to the Ltac tactic language. part: sections The section mechanism of Coq.
#18858 opened Mar 28, 2024 by Janno
1
ProTip! Adding no:label will show everything without a label.