[mutind] derive

[gares]

superseeds #1056

[Janno]

Originally posted by @gares in #890 (comment)

If you have time/energy, the main drill is to move code from .v to .elpi files and unify the entrypoint, as I did for the many derivations I merged

I tried to fix the test failure which seems to be due to missing support for mutual inductive types with parameters in param1_trivial. I think I got lost in the weeds somewhere trying to fix that (or get it fixed, rather). I am pretty short on time for the foreseeable future but I will try to extract a recipe for changes you mentioned in your comment and have the agents try their hands at that.

[gares]

I have just rebased on master to be sure all merged commits are gone