Adapt to coq PR #17991 which lets "simpl" refolds partial applications of fixpoints

[herbelin]

The simpl reduction used to not refold the partially applied recursive calls of reducible fixpoints as this was requiring eta-conversion. Thanks to eta-conversion support, this is not anymore needed and Coq PR coq/coq#17991 implements refolding of partial applications.

This has an impact on metacoq, in the file Typing.v of template-coq, namely, the expression

typing_size (type_App Σ Γ t l t_ty t' H e n t0)

reduces with the Coq PR to

S (Nat.max (typing_size H) (typing_spine_size (@typing_size cf) Σ Γ t_ty l t' t0))

while it reduced before to

S (Nat.max (typing_size H)
             (typing_spine_size
                (fun (x : global_env_ext) (x0 : context) 
                   (x1 x2 : term) (x3 : x;;; x0 |- x1 : x2) => 
                 typing_size x3) Σ Γ t_ty l t' t0

Assuming that the new behavior is "better" (more intelligible, more intuitive), this metacoq PR ensures that Typing.v compiles both with and without the change of behavior of simpl (the change is not very smart but works).

If ok for you, the PR can then be merged as soon as now.

[tabareau]

the new behavior looks indeed better