feat: Generate sort poly scheme with elim constraints

[TDiazT]

This PR adds the generation of an eliminator "_poly_rec" to sort-polymorphic inductives, leveraging elimination constraints to support any input and output sorts.

Existing "_rect", "_ind", etc., could be defined in terms of this one (for any sort, not just sort variables), but I think that'd be best in a separate PR.

Example:

Inductive nat@{s;|} : Type@{s;0} :=
| O : nat
| S : nat -> nat.

About nat_poly_rec.
(* nat_poly_rec@{α α0 ; u} :
forall (P : forall _ : nat@{α ; }, Type@{α0 ; u}) (_ : P O@{α ; })
  (_ : forall (n : nat@{α ; }) (_ : P n), P (S@{α ; } n)) 
  (n : nat@{α ; }),
P n *)
(* α α0 ; u |= α -> α0 *)

---

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• Opened overlay pull requests.

[TDiazT]

Need to recheck this. Probably extend build_case_analysis_scheme_in_type in the same way as the other.

[thomas-lamiaux]

looks alright to me

[TDiazT]

idem, recheck

[thomas-lamiaux]

This is not in your code, you do dependent by default

[thomas-lamiaux]

Can't you mege both functions as before by simply adding an element to elims ?

[TDiazT]

Yup, that's what I was doing before but, to be honest, a lot of the code in the original declare_one_induction_scheme was really adhoc for handling Type, Prop, and SProp specific cases.

For sort variables it's really short actually, so I preferred to separate them, making it easier to understand imo. I just renamed the original declare_one_induction_scheme to declare_one_induction_scheme_const but otherwise is the same code.