Adapt to https://github.com/coq/coq/pull/15341

[proux01]

To keep CI green once rocq-prover/rocq#15341 will be merged. This should be backward compatible so please merge whenever possible.

[bcpierce00]

Thanks. The actual changes need to be made upstream in the sfdev repo), so I'm going to close this PR here and port the changes there.

If you'd like access to the sfdev repo for future fixes, let me know.

I'll also need to re-release the PLF volume so that it gets pushed back here. Is that urgent?

[proux01]

Is that urgent?

Apparently it no longer is: rocq-prover/rocq#15341 (comment) and might even become useless. So I guess it is urgent to do nothing, sorry about that.

[bcpierce00]

No worries!

…

On Sat, Jul 15, 2023 at 5:26 AM Pierre Roux ***@***.***> wrote: Is that urgent? Apparently it no longer is: rocq-prover/rocq#15341 (comment) <https://urldefense.com/v3/__https://github.com/coq/coq/pull/15341*issuecomment-1635857450__;Iw!!IBzWLUs!WLdl6Bg_04PV9Rxk4qIgpfe5_Y-z6-h35S3_fWbeq5B2tn4JA-uuSSKS_1PEUifgboK4e06lT-1a9kwKA4iAaS2FW1zw$> and might even become useless. So I guess it is urgent to do nothing, sorry about that. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/DeepSpec/sf/pull/10*issuecomment-1636719654__;Iw!!IBzWLUs!WLdl6Bg_04PV9Rxk4qIgpfe5_Y-z6-h35S3_fWbeq5B2tn4JA-uuSSKS_1PEUifgboK4e06lT-1a9kwKA4iAafdOtygH$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC3RI6SKXSYLU64DF2TXQJO5XANCNFSM6AAAAAA2KJYNJ4__;!!IBzWLUs!WLdl6Bg_04PV9Rxk4qIgpfe5_Y-z6-h35S3_fWbeq5B2tn4JA-uuSSKS_1PEUifgboK4e06lT-1a9kwKA4iAafa2omDD$> . You are receiving this because you modified the open/close state.Message ID: ***@***.***>