recursively non-uniform parameters of inductive types #8
Description
The IsoRel translation currently does not support recursively non-uniform parameters of inductive types.
It assumes that parameters of an inductives are used uniformly. Since Coq 8.1, hypotheses of some constructors may use a different value for a parameter.
https://sympa.inria.fr/sympa/arc/coq-club/2010-05/msg00068.html
To handle such inductive types in the IsoRel translation, non-uniform parameters should be identified and treated like indices, which are already supported. According to the manual, recursively non-uniform parameters must be listed after the recursively uniform parameters:
https://coq.inria.fr/refman/Reference-Manual006.html#Cic-inductive-definitions (search "recursively non-uniform parameters")