coq
https://github.com/coq/coq
Triage Issues!
When you volunteer to triage issues, you'll receive an email each day with a link to an open issue that needs help in this project. You'll also receive instructions on how to triage issues.
Triage Docs!
Receive a documented method or class from your favorite GitHub repos in your inbox every day. If you're really pro, receive undocumented methods or classes and supercharge your commit history.
not yet supported7 Subscribers
Add a CodeTriage badge to coq
Help out
- Issues
- [declare] Warn on unused using attributes on sub-obligations
- Phrasing and formatting of the unsatisfiable constraints error message
- destruct produces an ill-typed term
- How to report the status of existential variables in a UI in the future?
- Warn when automatically lowering an inductive declared with `: Type` to Prop
- Search categories for constants with opaque (lemmas, etc) and transparent (definition, ...) bodies
- commit 5c94d0d375 breaks dependent evar line
- Conversion can fail to equate primitive projections with their compatibility constants
- experiment: measure gc time with ocaml 5 runtime events in newprofile
- ::> only declares an instance without a coercion when it should do both
- Docs
- not yet supported