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
- rocqide -xml-debug does not imply -debug
- rocqide get background goals when needed
- RocqIDE will report "All goals completed" when only a single subproof is complete
- Inline some constant arguments in rocqide
- Keep track of which variables are section variables and use this info to fix bugs
- `Extract Constant`, `Extract Inlined Constant`, `Extract Inductive`, `Extract Foreign Constant`, `Extract Callback` should support locality attributes and should not be superglobal by default
- Request: `From ... SafeRequire` (or `From ... RequireSafe`)
- Remove Context.Compacted.Declaration.to_named_context
- Stop relying on canonizing GlobRef.Map in hint internals.
- Remove unused APIs on named contexts
- Docs
- not yet supported