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
- Error: Anomaly "in Univ.repr: Universe SLF.LibRelation.22 undefined." on Scheme Elimination
- Experiment: optimized representation for `nat` constants (a zarith Z.t values)
- `Scheme All` fails on universally quantified arguments of constructors.
- `Scheme all` generates perfectible non-dependent eliminator when using `list_all` as an argument to a constructor
- Incorrect sort collapsing leading to type error
- Assert failure when declaring a global sort
- situations where setoid_rewrite in Type fails where it succeeds in Prop
- Use levels instead of separate entries for rewrite strategies
- Ssreflect rewrite with pattern with variable fails in a top-level Ltac definition
- Mark tactician allow_failure due to slow overlay merging
- Docs
- not yet supported