Optimize non-applicative stack nodes

[Tragicus]

When unifying terms that both have a Case, Fix or Proj node in their arguments stack, Coq tries to reduce the non-applicative stack node, so we know that the node will never be reduced unless an evar is instantiated. Hence we unify and remove the longest suffix of the stack containing applicative nodes or the last node if none exists.

Fixes / closes #????

• 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.

[Tragicus]

This should solve the performance issue in #19987.

[SkySkimmer]

@coqbot run full ci

[coqbot-app]

🔴 CI failures at commit 03c0916 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 818d1e0 succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-fiat_crypto, ci-hott, ci-unimath

• You can also pass me a specific list of targets to minimize as arguments.

[SkySkimmer]

@coqbot run full ci

[coqbot-app]

🔴 CI failure at commit dcac3d4 without any failure in the test-suite

✔️ Corresponding job for the base commit 25659d3 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-unimath

• You can also pass me a specific list of targets to minimize as arguments.

[SkySkimmer]

You can reopen if you get it to work, or if you can convince us that the failures are correct behaviour