Skip to content

Issues: rocq-prover/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

Clear current search query, filters, and sorts
71 Open 7 Closed
71 Open 7 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

int64 equivalent for ExtrOcamlIntConv
#3 opened Dec 21, 2024 by liyishuai
stdlib exports conflicting notations
#4 opened Dec 20, 2024 by andres-erbsen
ZifyBool overriding zify_post_hook is a bad idea
#6 opened Jun 5, 2024 by rlepigre
Scheme Equality for nat + Require Import Coq.Logic.Eqdep_dec. breaks inversion ("Illegal application" at Qed)
#8 opened Oct 2, 2023 by JasonGross
Conflicting use of "~=" in Coq.Program.Equality and Coq.Structures.Equalities
#16 opened Jul 31, 2022 by imaxw
Strong natural induction should be simpler
#22 opened Aug 10, 2021 by SnarkBoojum
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
Z.mod_mul_r and Z.rem_mul_r reversed
#31 opened Oct 30, 2019 by whonore
[stdlib] Modification of divisibility notation ( x | y ) in the stdlib.
#36 opened May 24, 2019 by ejgallego
Feature Request: setoid_rewrite should possibly work better with PERs
#42 opened Jul 28, 2018 by JasonGross
nsatz fails when Zpos is present
#44 opened Jun 29, 2018 by JasonGross
Order tactic fails when eq is defined in terms of le
#51 opened Feb 1, 2018 by dfoxfranke
Standard library equality schemes do not match [Scheme Equality]
#53 opened Jan 16, 2018 by JasonGross
How to transparently manage different naming schemes, or different ordering of arguments, etc. in libraries?
#55 opened Dec 1, 2017 by herbelin
Keep All.v in topological order
#106 opened Feb 12, 2025 by proux01
Bottlenecks in standard library
#9 opened Jul 20, 2023 by mrhaandi
1
Setoid rewriting hardcodes stdlib paths instead of relying on Register
#15 opened Nov 24, 2022 by Blaisorblade
1
Dep_elim database not used?
#20 opened May 19, 2022 by rnrand
1
binary and octal number notations
#23 opened May 6, 2021 by JasonGross
1
Require Import Int63 breaks Definition land := ...
#29 opened Mar 25, 2020 by JasonGross
1
NoDup List Cut Function
#30 opened Feb 28, 2020 by llee454
1
stdlib: Add FMap.min_elt
#39 opened Dec 8, 2018 by Lysxia
1
It should be easy to rewrite under binders with function extensionality
#41 opened Aug 16, 2018 by JasonGross
1
Improving the documentation of MSets
#47 opened Mar 25, 2018 by jad-hamza
1
ProTip! Type g i on any issue or pull request to go back to the issue listing page.