Control the transparency of compatibility constants via their projections.

[rlepigre]

This is roughly the first part of #18327.

• Added changelog.
• Added / updated documentation.
• Updated documented syntax by running make doc_gram_rsts.
• Opened overlay pull requests.

[herbelin]

The failure of bug_17774.v is easy to fix, isn't?

[rlepigre]

The failure of bug_17774.v is easy to fix, isn't?

Probably, I did not yet had the time to look into this.

[herbelin]

@coqbot run full ci

[coqbot-app]

🔴 CI failures at commit 8a8a22c without any failure in the test-suite

✔️ Corresponding jobs for the base commit ad8dda2 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-hott, ci-iris, ci-perennial, ci-unimath

• 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 targets (which I do not suggest minimizing):
  • ci-bedrock2 (because base job at ad8dda2 failed)
  • ci-jasmin (because base job at ad8dda2 failed)

[Janno]

@coqbot run full ci

[Janno]

@coqbot run full ci

[coqbot-app]

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

✔️ Corresponding jobs for the base commit c3306d6 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-hott, ci-iris, ci-perennial, ci-unimath

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

[Janno]

@coqbot run full ci

[coqbot-app]

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

✔️ Corresponding jobs for the base commit c3306d6 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-hott, ci-unimath

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

[Janno]

@coqbot run full ci

[rlepigre]

Closing since this is part of #18327.

[herbelin]

Maybe this PR would still be merged quicklier if kept independent from #18327.

[rlepigre]

Maybe this PR would still be merged quicklier if kept independent from #18327.

Possibly, but that would require to move the overlays here, and the other MR will hopefully be ready in the next few days (we were only stuck because the whole CI setup was broken).

[herbelin]

Possibly, but that would require to move the overlays here, and the other MR will hopefully be ready in the next few days (we were only stuck because the whole CI setup was broken).

I see. Another argument I can give otherwise is that reviewing the current PR would be easier than reviewing it together with #18327 (assuming that I correctly understand that it changes the infrastructure but a priori not the observational semantics).

[rlepigre]

I see. Another argument I can give otherwise is that reviewing the current PR would be easier than reviewing it together with #18327 (assuming that I correctly understand that it changes the infrastructure but a priori not the observational semantics).

I understand, but given that #18327 adds very little on top of this PR, and that it can still be easily reviewed by commit (with changes from this PR coming first), I don't think it is worth the extra effort to maintain two different PRs. But of course, if reviewing turns out to be too difficult, we can come back to taking two independent steps later.