Warn when automatically lowering an inductive declared with `: Type` to Prop

[SkySkimmer]

• option to disable the lowering and option to default declare dependent eliminators for inductives with explicit Prop (for compat when fixing the warning by putting explicit Prop)

Inductives with no explicit type (eg Inductive foo := C.) can still get silently put in Prop.

Maybe it would make sense to support _ as "pick Prop or Type as needed" to make it easier to port indexed inductives? eg Inductive foo : nat -> Type := . would become Inductive foo : nat -> _ := . (currently it fails saying "not an arity"). But it doesn't look that nice so probably not worth doing.

Funind behaviour is slightly changed as we now force its inductives in Type instead of letting them be lowered (forward compatible way to disable the warning).

Overlays:

• https://github.com/LPCIC/coq-elpi/pull/624

[SkySkimmer]

Maybe the options should be attributes instead, not sure.

[SkySkimmer]

@coqbot run full ci

[ppedrot]

@coqbot run full ci

[SkySkimmer]

category theory failure is spurious

[ppedrot]

@coqbot run full ci

[ppedrot]

@coqbot merge now

[coqbot-app[bot]]

@ppedrot: Please take care of the following overlays:

• 18989-SkySkimmer-warn-auto-lower.sh