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
- Partially applied template polymorphic inductive should warn
- Many missing manpages
- 1-field-record Typeclass syntax does not support implicit parameters
- Typeclass search distinguishes folded from unfolded primitive projections
- `coqtop` `-quiet` is less quiet in 8.14 than in 8.13
- custom entry printed as constr when `global` coercion is present
- Feature request: `Implicit Type` command with placeholders
- Debugger proof context display should show all goals in the same format used outside the debugger
- Interactive module should error when type is functorized
- Limitations of Qed on Let should be documented
- Docs
- not yet supported