Ltac2 Constr.Unsafe.case type should expose the inductive and the number of parameters

[JasonGross]

Description of the problem

It is useful when writing inversion-style automation to know how many parameters an inductive type should have. It is also sometimes important to know, given a match statement, which inductive is being matched. Hence there should be projections case -> inductive and case -> int (perahaps inductive_of_case and nbparameters_of_case?) which correspond to ci_ind and ci_npar in constr.mli¹ and to the tuple ind_and_nbparams in template-coq².

¹

coq/kernel/constr.mli

Lines 38 to 39 in e6991dc

	{ ci_ind : inductive; (* inductive type to which belongs the value that is being matched *)
	ci_npar : int; (* number of parameters of the above inductive type *)

² https://github.com/MetaCoq/metacoq/blob/1086391b66b82d10e9aa8d23411344ae9a49bbd4/template-coq/theories/Ast.v#L52

cc @ppedrot @andres-erbsen

Coq Version

master

[Zimmi48]

@ppedrot Do you intend to address this in time for 8.12? If that's the case, there should be an assignee. If not, please remove or adjust the milestone.

[ppedrot]

This is not urgent, so postponing.

[Zimmi48]

This was already postponed once. Not a problem, but maybe the milestone could be simply removed?

[samuelgruetter]

Having access to the number of parameters of an Inductive would be a useful feature!
Lack of this feature in Ltac 1 made me come up with hacks like this one, where I derive the number of parameters by checking for how many arguments passed to a constructor, the induction principle can be specialized with the argument (which is only the case for parameters, but not for indices).

[gares]

@ppedrot I'd like an update w.r.t. this PR and its milestone

[ppedrot]

It's an issue, not a PR, so postpone.

[gares]

My interpretation of milestoned issues, is that they have something to do with that release. So I'm not postponing, but rather clearing the milestone.