[ssr] Stop relying on camlp5 recovery mechanism

[proux01]

Stop relying on camlp5/coqpp recovery mechanism for "do [tac] => intro" and "tac; [tac|..|tac] => intro"

This is in preparation of #17876

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

Overlays (to be merged before the current PR)

• Adapt to https://github.com/coq/coq/pull/18224 math-comp/analysis#1088
• https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/536
• Update stdpp mit-pdos/perennial#58

Overlays (to be merged in sync with the current PR)

• Adapt to https://github.com/coq/coq/pull/18224 mattam82/Coq-Equations#578
• Adapt to https://github.com/coq/coq/pull/18224 MetaCoq/metacoq#1035
• Adapt to https://github.com/coq/coq/pull/18224 LPCIC/coq-elpi#586

[herbelin]

By the way, the notations .1 and .2 are extremely standard and should be reserved in Init (even if whether they apply to prod or sigT is not standardized... somehow we should eventually find a way to overload the notations for prod and sigT...).

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[herbelin]

Note: as future work for the notation system, we could think at how to define a notation x . N on lists or n-tuples which stands for hd (tl .. (tl x) ..) repeated N times. Something like:

Notation "x . N" := (hd (tl .. (tl x) ..)) (N meta-natural).

or maybe

Notation "x . N" := (hd (iter N tl x)) (eval iter on fixed N).

[proux01]

FWIW It's probably already possible to get something like (fun x => hd (tl ... (tl x)) x using number notations.

[proux01]

@coqbot run full ci

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[coqbot-app]

🔴 CI failures at commit 49b25ce without any failure in the test-suite

✔️ Corresponding jobs for the base commit 2af3ead 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-analysis, ci-equations, ci-iris, ci-perennial

• You can also pass me a specific list of targets to minimize as arguments.
• If you tag me saying @coqbot ci minimize all, I will additionally minimize the following target (which I do not suggest minimizing): ci-fiat_crypto_legacy (because base job at 2af3ead failed)

⚠️ ⌛ You may want to wait until the pipeline for the base commit (2af3ead) finishes.

[proux01]

@coq/ssreflect-maintainers this is finally ready (windows failure in CI is unrelated)

[ppedrot]

Let's explicitly ping @gares, I think this is an important foundational PR.

[ppedrot]

Ping @gares for assignee again, the sooner this is merged the better I think.

[proux01]

This s mostly a three lines PR, it shouldn't take much time to look at.

[gares]

@coqbot merge now

[coqbot-app]

@gares: Please take care of the following overlays:

• 18224-proux01-ssr_17876.sh

[SkySkimmer]

This seems to be a breaking change, why no changelog?

[proux01]

Indeed, here it is #18798