Jason Gross

> Will the Coq bug be fixed? I'm not sure. I certainly don't understand the code well enough to write a patch. @SkySkimmer [says](https://github.com/coq/coq/issues/17566#issuecomment-1534286791): > Old unification only understands inductive...

Can we get coqbot to minimize it for us? Something like @coqbot minimize coq.dev ```bash git clone [email protected]:JasonGross/coq-ext-lib.git --branch=cumul cd coq-ext-lib opam pin add -y . opam install -y coq-quickchick...

> > Fails QuickChick unit test on Coq dev: [QuickChick/QuickChick@`235f6f2`/test/plugin/plugin.v#L51](https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/test/plugin/plugin.v#L51) > > > File "./plugin.v", line 51, characters 0-22: > > > Error: Conversion test raised an anomaly: > >...

@liyishuai here's the minimized example. Any ideas for tracking down what's going on? Is QuickChick internally relying on some ext-lib structure not being cumulative? ------- @JasonGross, Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/QuickChick/test/plugin/plugin.v (full...

Slightly more minimal example. Removing `Cumulative` makes it pass ```coq Require Coq.Strings.String. Module Export Monad. Set Universe Polymorphism. Cumulative Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=...

Reported upstream as https://github.com/QuickChick/QuickChick/issues/352

I'm guessing the issue is that the `evd` from `interp_constr` is being thrown away in `let (c,_evd) = interp_constr env evd c in` https://github.com/QuickChick/QuickChick/blob/235f6f2156b06239d10e971b7f229f18b73fb67c/plugin/quickChick.mlg.cppo#L298-L302

The issue with loading prelude should not be a problem with Ltac2; we can just copy and replicate the `.v` files as `HoTT.Ltac2.*` or similar and it should work fine.

Note that removing the explicit `fig` object gets rid of the error

Note that this results in TeX capacity being exceeded on my example (n=64)