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
- Printing two notations that have the same RHS refers to them mutually
- `firstorder lia` fails with "No link."
- `tryif` treats "uncaught exception" anomalies as failures
- `firstorder congruence` fails with "reversible in 1st order mode"
- Recursive Extraction ignores Extraction Inline without Extract Constant, and extracts empty unused modules, resulting in invalid programs
- Assertion failure while defining Function
- [ssreflect] Error: Anomaly "The global environment cannot be accessed during parsing."
- btauto should not modify core HintDb
- `firstorder lia` is slow and fails with "reversible in 1st order mode"
- Proposal: -V option to handle package variants
- Docs
- not yet supported