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
- 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
- Add primitive string type.
- Unification ends in a stack overflow
- Fix occurrence checker not checking evar insts
- Add a PUSHACCMANY opcode.
- Docs
- not yet supported