Jan-Oliver Kaiser issues

Repositories
Issues
Comments

Results 22 issues of


                                            Jan-Oliver Kaiser

interp_context_gen: only solve locally created evars

More context here: https://coq.zulipchat.com/#narrow/channel/253928-Elpi-users-.26-devs/topic/context-decl.20changes.20in.20Coq.208.2E20.3F/near/477391848 I don't think the bug can be triggered without a plugin - [ ] Added / updated **test-suite**. - [ ] Added **changelog**. - [ ]...

kind: fix

Hint Resolve registers the same hint for a definitional class multiple times at different patterns

### Description of the problem `Hint Resolve` is a little overeager and finds multiple possible patterns for hints whose type ends in definitional classes. `Existing Instance` does not have this...

part: typeclasses

kind: bug

needs: triage