Trying to recompute the inductive structure of the main (co)-inductive types when checking the guard condition

[herbelin]

This should have been done for a very long time already: we recompute dynamically the recursive structure of the decreasing argument of fixpoints.

We could have introduced a notion of parametric recursive structure (precomputed "recarg") and instantiate the parameter dynamically (this is what we made in a first attempt of the PR actually), however we would have failed to support examples requiring a computation after instantiation of the parameters as in:

Inductive list (b : bool) A B :=
| nil : list b A B
| cons : (if b then A else B) -> list b A B -> list b A B.

Inductive tree := Foo : list true tree unit -> tree.

Fixpoint f (l : list true tree unit) {struct l} :=
  match l with
  | nil _ _ _ => 0
  | cons _ _ _ (Foo l') _ => f l'
  end.

Closes #9045, #12781, #13855, #15932.

• Added / updated test-suite.
• Added changelog.

Depends on #18229 and #18242.

To do:

• double-check that we are not doing something wrong
• check performance, possibly compute recargs lazily
• decide if precomputation of recargs is still useful

[herbelin]

@coqbot: run full ci

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.