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
- refine loses unification constraints where reflexivity does not
- Infinite loop in Coq's type inference?
- [vm/native] -no-naked-pointers support
- CoqIDE script panel display can get confused about what has been proven (+CoqIDE debugger)
- `symmetry` gives confusingly bogus unification errors on eq-like inductives with no `Symmetry` instance.
- 'ring_simplify term in hyp' makes definition opaque
- `ring` creates invalid proof term if section variable is reverted and re-intro'd with the same name
- coq_makefile fails to handle generated files when computing ml dependencies
- Set Implicit Arguments vs Typeclasses
- Deprecated operconstr to term but different functionality
- Docs
- not yet supported