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
- Bad generalization by dependent induction in Section
- Generalized rewriting support for "respectful_hetero"
- Doubled "Trying to mask the absolute name" warning
- Ltac2 unsafe_constr scope
- `Qed` is 40x slower than `Defined` because of private universes
- Abort in nested proofs doesn't work the first time.
- Ssreflect `rewrite` overeagerly normalizes `match`/`if` in subterm seletion
- Ltac2 anomaly unbound variable / uncaught Not_found with `constr:(ltac:(ltac2:(some_var)))`
- `Coercion` should support `#[export]`
- Info message for `Scheme Induction` is incorrect for non-recursive types
- Docs
- not yet supported