Jason Gross
Jason Gross
You can probably minimize this with [the bug minimizer](https://github.com/JasonGross/coq-tools)
Does coqbot watch this repo? @coqbot minimize ``` opam install coq-metacoq coq-quickchick echo > bug.v
I guess not. Trying at https://github.com/coq-community/run-coq-bug-minimizer/issues/2#issuecomment-982842826
Can metacoq do a release so that the opam package is compatible with 8.14.0?
If indeed this is the issue, the solution is to eta-expand `list` everywhere it's used as a function, as I say at https://github.com/coq-community/coq-ext-lib/pull/123#discussion_r783590882
Is there an enumeration somewhere of what code the kernel actually depends on? (I thought the point of having `kernel/` vs other directories was to have a clear(er) separation between...
This is ready for review and merge. Can I get an assignee?
Should be ready for review and merge, sorry for the delay
> the interface you refer to isn't able to support debugging tactics that combine Ltac with Ltac2 Is this already a problem with debugging interleaved `Hint Extern` calls via typeclass...
> If you're referring to `auto` invoking both Ltac and Ltac2 tactics, currently the debugger stack and variables won't show any info on any Ltac2 tactics or any indication that...