Skip to content

Issues: coq/stdlib

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

68 Open 3 Closed
68 Open 3 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

stdlib wastes time being rebuilt on every minimizer run
#98 opened Jan 27, 2025 by JasonGross
4
int64 equivalent for ExtrOcamlIntConv
#3 opened Dec 21, 2024 by liyishuai
stdlib exports conflicting notations
#4 opened Dec 20, 2024 by andres-erbsen
Confusing warning: Using Vector.t is known to be technically difficult
#5 opened Dec 7, 2024 by cogumbreiro
5
ZifyBool overriding zify_post_hook is a bad idea
#6 opened Jun 5, 2024 by rlepigre
Hard to fix Stdlib arithmetic deprecations in 8.18 breaking many projects in 8.19
#7 opened Jan 3, 2024 by palmskog
18
Scheme Equality for nat + Require Import Coq.Logic.Eqdep_dec. breaks inversion ("Illegal application" at Qed)
#8 opened Oct 2, 2023 by JasonGross
Bottlenecks in standard library
#9 opened Jul 20, 2023 by mrhaandi
1
List.rev is unexpectedly quadratic
#10 opened Jul 12, 2023 by charguer
3
ListNotations breaks primitive array syntax
#11 opened Jul 5, 2023 by JasonGross
5
Import Nsatz redefines "0" and "1"
#12 opened May 29, 2023 by andres-erbsen
6
Search Blacklist lemmas generated from Add Field
#13 opened Dec 23, 2022 by Villetaneuse
2
Missing lemmas about Prop: absorbing or neutral elements for various operations
#14 opened Dec 14, 2022 by SnarkBoojum
3
Setoid rewriting hardcodes stdlib paths instead of relying on Register
#15 opened Nov 24, 2022 by Blaisorblade
1
Conflicting use of "~=" in Coq.Program.Equality and Coq.Structures.Equalities
#16 opened Jul 31, 2022 by imaxw
coqc infinite loop in type class resolution
#17 opened Jun 20, 2022 by larsr
8
The Standard Library should not be adding transitivity and symmetry hints to core
#18 opened Jun 3, 2022 by JasonGross
1
3
Dep_elim database not used?
#20 opened May 19, 2022 by rnrand
1
Require Import Coq.Sorting.Permutation. slows down rewrite_strat > 10x
#21 opened Feb 17, 2022 by samuelgruetter
7
Strong natural induction should be simpler
#22 opened Aug 10, 2021 by SnarkBoojum
binary and octal number notations
#23 opened May 6, 2021 by JasonGross
1
Cannot pattern match on exist in program definitions
#24 opened Apr 23, 2021 by Tuplanolla
incl_dec and NoDup_dec should be Defined and not Qed
#25 opened Apr 21, 2021 by jjhugues
1
btauto should not modify core HintDb
#27 opened Jul 14, 2020 by samuelgruetter
4
definition of field and ring theories excluded from standard library reference main page
#28 opened Apr 16, 2020 by MSoegtropIMC
3
ProTip! Mix and match filters to narrow down what you’re looking for.