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
- Scoped infix notation for Ltac2 operators
- `Hint Constants Opaque : typeclass_instances` results in nonsensical failure messages from `Set Typeclasses Debug Verbosity 2`
- Unification leaves unbound de Bruijn index
- Support extraction of template-polymorphism types in Prop by means of coercions
- Canonical part of constant forgotten when inlinable constant is 'overridden' by non-inlinable constant.
- Feature request: Register Ltac2 ident1 as ident2
- FR: build coq using dune without coqide dependencies
- Incorrect opaque state with nested proofs
- Ltac2 tactic for determining if an `ident list` refers to a functor, bound functor argument, module type, or not
- `cbn` and `/=` have different behaviors when `SimplIsCbn`
- Docs
- not yet supported