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 supported9 Subscribers
Add a CodeTriage badge to coq
Help out
- Issues
- No tooltip appears for syntax errors
- Stack overflow in parsing when introducing an Ltac2 notation
- Definitional classes don't produce notice
- Ltac2 should reject double declaration of external at a given name
- surprising unification of Type with Prop/SProp in inductive elaboration
- "bad case inversion" error with sort polymorphism
- Not_found when loading a vo, a priori in relation with files compiled with a different version of coqc
- There is no command to print currently available modules.
- Make it possible to enable/disable a `String Notation`
- [experiment] Convert arguments in the right order in kernel.
- Docs
- not yet supported