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
- Incorrect error "Command not supported (Open proofs remain)" in async mode
- Faulty universe check in subtyping function
- [core] Improved state protection against memprof-limits interruptions
- `ltac:( )` quotation no longer supported in `change`
- Parse `Type@{ Prop/SProp/Set | ... }` rather than failing
- scope annotation are not considered for printing width
- The syntax `Type@{ Set/Prop/SProp | ...}` should be accepted as well by Coq
- No tooltip appears for syntax errors
- Stack overflow in parsing when introducing an Ltac2 notation
- Definitional classes don't produce notice
- Docs
- not yet supported