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
- Allow open terms in "apply ->" and "apply <-" (fix #18177).
- Anomaly "in Lemmas.save_lemma_admitted: more than one statement." with Derive
- Synterp code of creating notations unnecessarily uses notation's body
- [unification] Experiment: add a flag to configure conversion on heads found by FO approximation
- Poor compilation of dependent pattern-matching in bytecode
- Return canonical instance from basic declare.ml APIs + use to fix Program bug
- Fix support of Program-style pattern-matching for multiple arguments in inductive families
- Ltac2: provide access to boxing API in printf
- Coq does not use the notation for printing (with custom entries)
- Map opaque definitions to lossy accumulators in the VM
- Docs
- not yet supported