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
- `lia` cache should not use OCaml type-unsafe marshalling functions
- Feature request: check argument names before checking arguments count in Arguments … : assert.
- Location information for warning variable-collision,ltac should be more precise
- "fix" tactic may produce ill formed terms
- [sphinx] Rendering issues in coqtop blocks when using bullets and indentation.
- Z.mod_mul_r and Z.rem_mul_r reversed
- Warning: Collision between bound variable x and a metavariable of same name. [meta-collision,ltac] should trigger at Ltac definition time, not running time
- [API] Coqlib.lib_ref raises UserError
- Windows installer fails to install OCaml binaries; coq_makefile emits a non-existant location for ocamlfind on Windows
- Time to failure of rewrite depends on size of expanded term (regression somewhere between 8.4 and 8.7.2)
- Docs
- not yet supported