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 supported5 Subscribers
Add a CodeTriage badge to coq
Help out
- Issues
- Move rewrite_db tactic in doc
- Stop caring about unfolding state of primproj in constr_matching
- improve deprecation message for minus_plus
- Automatic bidirectionality hints
- Generalizing "Load ident" into "Load qualid" and clarifying difference with "Load file"
- `match` (`pattern_of_constr`?) depends on whether or not an evar was created before or after the most recent `.`
- A parametricity-style algorithm for automatic generation of Boolean equality associated to an inductive type
- Hide the instantiation of patterns with constr variables under an API.
- Make Scheme Equality compatible with universe polymorphism
- Support for inductive with defined parameters in native_compute
- Docs
- not yet supported