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,499 Open 7,417 Closed
2,499 Open 7,417 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

Multiple tactics cannot handle sort-polymorphic registered equality. kind: bug An error, flaw, fault or unintended behaviour.
#19203 opened Jun 12, 2024 by jpoiret
Incorrect error "Command not supported (Open proofs remain)" in async mode kind: bug An error, flaw, fault or unintended behaviour. part: CoqIDE Issues and PRs related to CoqIDE or other IDE features of coq. part: STM State Transition Machine, asynchronous proofs, etc.
#19189 opened Jun 8, 2024 by jfehrle
ltac:( ) quotation no longer supported in change kind: bug An error, flaw, fault or unintended behaviour. part: ltac Issues and PRs related to the Ltac tactic language.
#19182 opened Jun 7, 2024 by vfukala
3
Faulty universe check in subtyping function kind: bug An error, flaw, fault or unintended behaviour.
#19178 opened Jun 7, 2024 by ppedrot
1
scope annotation are not considered for printing width kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Improvement of error messages, new warnings, etc.
#19168 opened Jun 7, 2024 by Matafou
5
"destauto" tactic has a hard-coded dependency on a variable named "x" 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: tactics
#19167 opened Jun 7, 2024 by jfehrle
The syntax Type@{ Set/Prop/SProp | ...} should be accepted as well by Coq kind: wish Feature or enhancement requests. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#19162 opened Jun 6, 2024 by kyoDralliam
1
1
casts incorrectly refresh universes kind: bug An error, flaw, fault or unintended behaviour.
#19161 opened Jun 6, 2024 by kyoDralliam
1
3
github: Projects (classic) will be sunset on August 23, 2024 kind: infrastructure CI, build tools, development tools.
#19156 opened Jun 6, 2024 by SkySkimmer
Tooltip for syntax errors is highlighted but not displayed 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: CoqIDE Issues and PRs related to CoqIDE or other IDE features of coq.
#19152 opened Jun 5, 2024 by jfehrle 8.20+rc1
1
ZifyBool overriding zify_post_hook is a bad idea 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. part: standard library The standard library stdlib.
#19150 opened Jun 5, 2024 by rlepigre
No tooltip appears for syntax errors 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: CoqIDE Issues and PRs related to CoqIDE or other IDE features of coq.
#19139 opened Jun 4, 2024 by jfehrle
Ltac2's Control.new_goal leaves new goal on the shelf spuriously kind: bug An error, flaw, fault or unintended behaviour. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
#19138 opened Jun 4, 2024 by Janno
1
1
Stack overflow in parsing when introducing an Ltac2 notation part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. part: parser
#19130 opened Jun 2, 2024 by afdw
1
Definitional classes don't produce notice kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Improvement of error messages, new warnings, etc.
#19118 opened May 30, 2024 by Alizter
1
Ltac2 should reject double declaration of external at a given name kind: bug An error, flaw, fault or unintended behaviour. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
#19110 opened May 29, 2024 by SkySkimmer
surprising unification of Type with Prop/SProp in inductive elaboration kind: bug An error, flaw, fault or unintended behaviour.
#19079 opened May 24, 2024 by SkySkimmer
"bad case inversion" error with sort polymorphism kind: bug An error, flaw, fault or unintended behaviour.
#19070 opened May 22, 2024 by SkySkimmer
8
Not_found when loading a vo, a priori in relation with files compiled with a different version of coqc kind: bug An error, flaw, fault or unintended behaviour. kind: regression Problems that were not present in previous versions.
#19055 opened May 19, 2024 by herbelin
8
Make it possible to enable/disable a String Notation kind: wish Feature or enhancement requests. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
#19043 opened May 17, 2024 by gmalecha
There is no command to print currently available modules. kind: wish Feature or enhancement requests. part: modules The module system of Coq. part: vernac High level command interpretation.
#19035 opened May 16, 2024 by Villetaneuse
Allow Program to be used with noinit kind: feature New user-facing feature request or implementation. part: noinit Issues and PRs about the -noinit flag, which loads coq without the stdlib. part: program
#19033 opened May 15, 2024 by Alizter
4
destruct produces an ill-typed term kind: bug An error, flaw, fault or unintended behaviour.
#19004 opened May 6, 2024 by mrhaandi
3
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
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
ProTip! Updated in the last three days: updated:>2024-06-09.