RFC: Split stdlib Program into Init and deprecated

[andres-erbsen]

On top of #19797

• Added changelog.
• Added / updated documentation.
• Opened overlay pull requests.
  • "Basics" module name collision
• Replace remaining internal uses of newly deprecated tactics with existing tactics

[coqbot-app]

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

✔️ Corresponding job for the base commit 7e4ae8f 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-paramcoq

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

[andres-erbsen]

Definition fix_proto {A : Type} (a : A) := a.
Register fix_proto as program.tactic.fix_proto.

Is this required for Program to work well? Right now it's the only Register in a to-be-deprecated file.

[herbelin]

Is this required for Program to work well?

It is used at elaboration time as a marker to control the Program obligation tactics, so it really goes together with the Program set of tactics. If not a problem, I would say that it is simpler for these tactics to work if it can be kept.

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

[proux01]

Stdlib is now in its own repo: https://github.com/coq/stdlib , if this PR is still current, please reopen it there.